Title: Theory / Unimportant / CS / Fundamental / WQO

Name: Quasi-ordering on \(X\)
Definition: A reflexive transitive relation
Page: 1
Variables: \(X\) a set
Name2: Preorder on \(X\)

Name: An ordering on \(X\)
Definition: An antisymmetric quasi-ordering
Page: 1
Variables: \(X\) a set

Name: A quasi-order
Definition: A set and a quasi-ordering on it
Page: 1
Abbreviation: qo

Name: An order
Definition: A set and an ordering on it
Page: 1
Name2: A poset

Name: A linear qo
Definition: A quasi-order such as each pair of elements are comparable
Page: 1
Name2: A total qo

Name: comparable elements
Definition: Elements \(x,y\) such that either \(x\le y\) or \(y\le x\)
Page: 1
Variables: \(X,\le\) a qo

Definition: \(x\le y\) and \(y\le x\)
Page: 1
Variables: \(X,\le\) a qo
Notation: \(x\equiv y\)

Name: A terminating relation on \(X\)
Definition: \(\to\) binary relation on \(X\) such that there exists no infinite sequence \(x_0\to x_1\to\dots\)
Page: 1
Variables: \(X\) a set

Name: A well-founded qo on \(X\)
Definition: A qo such that \(>\) is terminating
Page: 1
Variables: \(X\) a set

Name: An antichain
Definition: A set of pairwise incomparable elements of \(X\)
Page: 1
Variables: \(X, \le\) a qo

Name: A good sequence
Definition: An infinite sequence \(x_0,x_1,\dots\) such that there is a pair \(i<j\) such that \(x_i\le x_j\)
Page: 1
Variables: \(X, \le\) a qo
Context: QO

Name: A well qo on \(X\)
Definition: such that every infinite sequence \(x_0,x_1,\dots\) is good
Page: 1, 2, 3
Chapter: 1
Variables: \(X\) a set
Index: 5, 7
Kind: Theo, prop
Definition2: every infinite sequence has a monotone (non-decreasing) subsequences
Definition3: with no infinite antichain
Abbreviation: wqo
Definition4: for every upwards-closed subset MmA there is a finite antichain \(A_0\) such that \(\uparrow A_0=A\)
Definition5: such that infinite monotone sequences of upwards-closed subset are stationnary
DefType: A qo \(\le\)
Definition6: such that the subset relation on downward-closed set is a well-founded order

Smaller0: total well-founded
Greater0: well-founded
Page: 1
Variables: \(X,  \le\) a set
Prefix Greater: \(\le\) is
Counterexample: \(=\) as qo over \(\mathbb N\) or \(\{0,1\}\)
Intermediate: \(\le\) is well

Name: A monotone sequence
Definition: A sequence \(x_0\le x_1\le x_2\le\dots\)
Page: 2
Variables: \(X,\le\) a qo

Name: An upward/downward closed subset of \(X\)
Definition: A set \(A\subseteq X\) such that for each \(a\in A\) and \(a\le x\)/\(a\ge x\), \(x\) belongs to \(A\)
Page: 3
Chapter: 1
Variables: \(X,\le\) a qo

Definition: The smallest upward/downward-closed subset containing \(A\)
Page: 3
Chapter: 1
Variables: \(X,\le\) a qo
\(A\subseteq X\)
Notation: \(\uparrow A\) \(\downarrow A\)
Definition2: The set of all \(x\in X\) such that \(a\le x\) for some \(a\in A\)

Name: A basis of \(A\)
Definition: A finite subset \(S\subseteq A\) such that \(\uparrow S=A\)
Page: 3
Chapter: 1
Variables: \(X,\le\) a qo
\(A\subseteq X\)
Assuming: \(A\) is upward closed

Smaller0: a upward closed set
Greater0: a downward closed set
Page: 4
Chapter: 1
Variables: \(X,\le\) a qo
Index: 10
Kind: Lem
Smaller to greater: is the complement of

Name: wqo
Page: 5
Section: 1
Index: 10
Kind: Lem
Closure: contains
Under: finite set
Closure2: sum
Condition2: finite disjoint
Closure3: product
Condition3: finite
Closure4: multiset \(\le_\ostar\)
Closure5: multiset extension
Closure6: trees
Closure7: words and embedding (\(\le_*\))
Closure8: hoare extension
Closure9: subset
Closure10: surjective monotonic map

Definition: the qo over the set \((i,x)\) with \(x\in D_i\) and \((i,x)\le (j,y)\) iff \(i=j\) and \(x\le y\)
Page: 5
Chapter: 1
Variables: \(X_i,\le_i\) qo
Notation: \(\sum_{i}D_i\)
Kind: Lem

Definition: The qo with set \(\prod_iX_i\) and \((x_i)\le (y_i)\) iff for each \(i\), \(x_i\le y_i\)
Page: 5
Chapter: 1
Variables: \(X_i,\le_i\) qo
Notation: \(\prod_{i}D_i\)
Kind: Lem

Name: wqo on \(X\)
Page: 5
Section: 1
Variables: \(X\) a set
Kind: Lem
Closure: extension
Closure2: intersection
Condition2: finite

Name: The embedding of \(\le\) on \(X^*\)
Definition: the relation containing \((x_1\dots x_n),(w_0y_1w_1\dots w_nx_n)\) with\(x_i\le y_i\in X\)  and \(w_i\in X^*\)
Page: 6
Chapter: 1
Section: 4
Variables: \(X, \le\) a qo
Notation: \(\le_*\)
Kind: Lem

Name: The embedding of \(\le\) on \(X^ostar\)
Page: 6
Chapter: 1
Section: 4
Variables: \(X, \le\) a qo
Notation: \(\le_\ostar\)
Kind: Lem

Name: The multiset extension of \(\le\) on \(X^ostar\)
Definition: The qo on \(X^\ostar\) containing \((m,n)\in X^\ostar\) iff for each \(x\in m\), either \(m(x)\le n(x)\) or there exists \(x<y\in n\)
Page: 6
Chapter: 1
Section: 4
Variables: \(X, \le\) a qo
Notation: \(\le_{\text{mul}}\)
Kind: Lem

Name: The hoare qo
Definition: containing \((D, E)\) if for each \(d\in D\) there exists \(d\le e\in E\)
Page: 9
Chapter: 1
Section: 5
Variables: \(X, \le\) a qo
Notation: \(\le^♭\)
Kind: Lem
Definition2: Restriction of multiset extension to set
Definition3: containing \((D, E)\) iff \(\downarrow D\subseteq\downarrow E\)
DefType: The qo on \(\mathcal P_f(X)\)

Name: Rado's structure
Definition: The wqo on \(\mathbb N^2\) containing \((m,n),(m',n')\) if (\(m=m'\) and \(n\le n'\)) or \(n< m'\)
Page: 9
Chapter: 1
Section: 4
Notation: \(R\)
Kind: Lem

Name: The homeomorphic embedding of \(\le\)
Page: 11
Chapter: 1
Section: 6
Notation: \(\le_T\)
Extra: \(D\) a signature of terms \(t_i\) with arity \(a_i\)
\(\le\) a qo over \(\{t_i\}\)

Question: Example of WQO
Answer: finite set
Page: 11
Chapter: 1
Section: 6
Answer2: undirected graph and minor
Answer3: finite words and subword

Name: A directed subset of \(X\)
Definition: every finite subset of \(A\) has an upper bound in \(A\)
Page: 13
Chapter: 1
Section: 8
Variables: \(X,\le\) a qo
Definition2: for every pair of elemenst \(x,y\in A\) there is \(z\in A\) such that \(x,y\le z\) and \(A\)
DefType: A non-empty finite subset \(A\subseteq X\) such that

Name: dcpo
Definition: A poset where every directed family has a least upper bound
Page: 13
Chapter: 1
Section: 8

Name: A Scott-continous function
Definition: monotonic
Page: 13
Chapter: 1
Section: 8
Context: dcpo
Definition2: preserves directed suprema, in the sense that for every directed family \((x_i)_{i\in I}\) in \(X\), \(\sup_{i\in I}f(x_i)=f(\sup_{i\in I}x_i)\)
DefType: A function \(f\) between dcpos

Name: An ideal
Definition: directed downward-closed
Page: 14
Chapter: 1
Section: 8
Variables: \(X,\le\) a qo
Definition2: irreducible downwards-closed
DefType: A subset of \(X\)

Name: An irreducible set
Definition: non-empty and for all downwards-closed subsets \(D_1,D_2\) such taht \(A\subseteq D_1\subseteq D_2\), \(A\) is already contained either in \(D_1\) or \(D_2\)
Page: 14
Chapter: 1
Section: 8
Variables: \(X,\le\) a qo
Definition2: \(A\) is irreducible iff it's non-empty and for any two upwards-closed subsets \(U_1,U_2\), if \(A\) intersects each of \(U_1,U_2\), then it intersects \(U_1\cap U_2\)
Example: one-point set
Example2: \(\downarrow x\) for \(x\in X\)
Example3: \(\subseteq_{n\in\mathbb N}\downarrow x_i\) for \((x_i)\) an infinite strictly increasing chain
DefType: A subset \(A\subseteq X\)

Name: A principal ideal
Definition: \(\downarrow x\) for some \(x\in X\)
Page: 14
Chapter: 1
Section: 8
Variables: \(X,\le\) a qo

Name: The ideal completion of \(X\)
Definition: the dcpo whose elements are ideals of \(X\) ordered for inclusion
Page: 15
Chapter: 1
Section: 8
Variables: \(X,\le\) a qo
Notation: \(Idl(X)\)

Name: Well structured transition systems
Definition: \(\le\) a wqo
Page: 15
Chapter: 1
Section: 9
Variables: \(X,\le\) a qo
Definition2: \(s\to s'\) and \(s\le t\) implies \(\exists t'\ge s'\) with \(t\to t'\)
Example: VASS
Abbreviation: WSTS
Intuition: The \(\ge\)-larger states can simulate the \(\to\)-
behaviour of smaller states
DefType: A triple \(S,\le,\to\) with

Name: A \(d\)-dimensional Vector addition system with states
Definition: A finite set \(Q\)
Page: 16
Chapter: 1
Section: 9
Definition2: \(\delta\subseteq Q\times\mathbb Z^d Q\) a finite set of translations
Definition3: \(q_0\in Q\)
Abbreviation: VASS
Definition4: \(\mathbr{x}_0\)

Name: A transition in this vass
Definition: \((q,\mathbr x)\to(q,\mathbr x')\) with \((q,\mathbr{x'-x},q')\in\delta\)
Page: 16
Chapter: 1
Section: 9
Variables: \(\langle Q,\delta,q_0, \mathbr x_0\rangle\) a VASS

Name: \(S\) terminates on \(s_0\)
Definition: Each sequence \(s_0\to s_1\to\dots\) terminates
Page: 16
Chapter: 1
Section: 9
Variables: \(S=\langle S,\to,\le\rangle\) a WSTS
\(s_0\in S\)

Name: the exisnestial succesor set
Definition: \(\{s'\in S\mid s\to s'\}\)
Page: 16
Chapter: 1
Section: 9
Variables: \(S=\langle S,\to,\le\rangle\) a WSTS
\(s_0\in S\)
Notation: \(Post(s)\)

Name: A post-effective WSTS
Definition: A WSTS such that for each \(s\), \(Post(s)\) is computable
Page: 16
Chapter: 1
Section: 9

Name: \(S\) is image finite
Definition: \(Post(S)\) is finite for each \(s\in S\)
Page: 16
Chapter: 1
Section: 9
Variables: \(S=\langle S,\to,\le\rangle\) a WSTS

Question: How to decide whether \(S\) terminates from \(s\)
Answer: Generate the tree of possible path. If the tree is finite, accept
Page: 17
Chapter: 1
Section: 9.1
Variables: \(S=\langle S,\to,\le\rangle\) a WSTS
\(s\in S\)

Question: How to decide whether \(S\) does not terminate from \(s\)
Answer: Generate the tree of possible path, if there is a path \(t\to t'\) with \(t\le t'\), accepts
Page: 17
Chapter: 1
Section: 9.1
Variables: \(S=\langle S,\to,\le\rangle\) a WSTS
\(s\in S\)

Name: The coverability problem
Definition: Given two states \(s,t\in S\), is there a finite path \(s=s_0\to s_1\to\dots\to s_n\ge t\)?
Page: 17
Chapter: 1
Section: 9.1
Variables: \(S=\langle S,\to,\le\rangle\) a WSTS

Name: upwards-closed sets of states
Page: 18
Section: 9.2
Chapter: 1
Variables: \(X,\le\) a wqo
Under: \(pre_\exists\)

Definition: \(\{s\in S\mid\exists s'\in U, s\to s'\}\)
Page: 18
Chapter: 1
Section: 9.2
Variables: \(S,\to\) a state system
\(s\in S\)
Notation: \(Pre_\exists(U)\)

Name: A pred-basis of \(s\)
Definition: A finite basis of \(\uparrow Pre_\exists(\uparrow\{s\})\)
Page: 18
Chapter: 1
Section: 9.2
Variables: \(S,\to\) a state system
\(s\in S\)
Notation: \(pb(s)\)

Name: A ranking function
Definition: A function \(\rho:S\to F\) with \(F\) a qo
Page: 18
Chapter: 1
Section: 10
Variables: \(S,\to\) a state system

Question: How to use ranking function to prove \(S\) terminates
Answer: Use a ranking function \(\rho:S\to (X,\le)\) a well founded order and show that \(x\to y\) implies \(\rho(x)<\rho(y)\)
Page: 20
Chapter: 1
Section: 10
Variables: \(S,\to\) a state system
Answer2: Use a ranking function \(\rho:S\to (X,\le)\) a wqo order and show that \(x\to^* y\) implies \(\rho(x)\not\ge\rho(y)\)