Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized

Definition 18.10Partial solution

A partial solution $(L_{0}^{'}, ⋄^{'}, S^{'}, I)$ is a collection of the following data:

A partially defined function $L_{0}^{'} : N \to N$ , defined on a finite union of right cosets of $⟨ e_{0} ⟩$ ;
A partially defined operation $⋄^{'} : N \times N \to M$ , defined on a finite set;
A partially defined function $S^{'} : N \to S M$ , defined on a finite set; and
A finite collection $I$ of “pending identities” $I [x, y, z]$ , which one can think of either as ordered triples of elements $x, y, z \in N$ , or as formal strings of the form “ $z ⋄^{'} x = (R_{2 S^{'} x}^{'})^{- 1} L_{0}^{'} R_{0}^{'} R_{S^{'} x}^{'} y$ ” for some $x, y, z \in N$ .

Furthermore, the following axioms are satisfied:

(i”) $L_{0}^{'} x$ is defined and equal to $y$ , then we have the identities Equation 6, Equation 7 for all $n \in Z$ .
(S) If $S^{'} x$ is defined for some $x \in N$ , then $S^{'} y$ is defined for all $y \leq x$ .
(iii”) If $R_{a}^{'} x = y$ for some $a \in S M$ and some $x, y \in N$ , and $S^{'} x, S^{'} y$ are defined, then $(R_{S^{'} y}^{'})^{- 1} L_{0}^{'} R_{2 S^{'} y}^{'} (R_{a - S^{'} x}^{'})^{- 1} L_{0}^{'} R_{2 (a - S^{'} x)}^{'} y$ is defined and equal to $x$ .
(iv”) If $x \in N$ is such that $S^{'} x$ is defined, then $(R_{S^{'} x}^{'})^{- 1} L_{0}^{'} R_{2 S^{'} x}^{'} (R_{S^{'} x}^{'})^{- 1} L_{0}^{'} R_{2 S^{'} x}^{'} x$ is defined and equal to $x$ .
(v”) If $x \in N$ and $x ⋄^{'} x$ is defined, then $S^{'} x$ is defined and equal to $x ⋄^{'} x$ .
(vi”) For all $y \in N$ and $a \in S M$ , if $R_{a}^{'} y ⋄^{'} y$ is defined, then $a - S^{'} y$ is defined and equal to $R_{a}^{'} y ⋄^{'} y$ .
(vii”) For all $x, y \in N$ and $x$ is not equal to $y$ or $R_{a}^{'} y$ for any $a \in S M$ , and $x ⋄^{'} y$ is defined, then it is equal to some $z \in N$ . Furthermore, either $I [x, y, z]$ is a pending identity, or else $z ⋄^{'} x$ and $(R_{2 S^{'} x}^{'})^{- 1} L_{0}^{'} R_{0}^{'} R_{S^{'} x}^{'} y$ are defined and equal to each other.
(P) If $I [x, y, z]$ is a pending identity, then $x, y, z \in N$ , and $S x$ and $z ⋄^{'} x$ are undefined. Furthermore, $z$ is not equal to $x$ or $R_{a}^{'} x$ for any $a \in S M$ , and $y$ is not of the form $(R_{0}^{'})^{n} x$ or $(R_{0}^{'})^{n} y_{0}$ for any $n$ , where $y_{0}$ is the parent of $x$ .
(P’) If $I [x, y, z]$ and $I [x, y^{'}, z]$ are pending identities, then $y = y^{'}$ .
(P”) If $I [x, y, z]$ is a pending identity, then $x ⋄^{'} y = z$ .
(L) If $y$ is the parent of $x$ with $x = R_{a}^{'} y$ , and $(R_{a - S^{'} y}^{'})^{- 1} L_{0}^{'} R_{2 (a - S^{'} y)}^{'} x$ is defined, then it is not equal to $x$ .

We say that one partial solution $({\tilde{L}}_{0}^{'}, {\tilde{⋄}}^{'}, {\tilde{S}}^{'}, \tilde{I})$ extends another if $(L_{0}^{'}, ⋄^{'}, S^{'}, I)$ if ${\tilde{L}}^{'}$ is an extension of $L_{0}^{'}$ , ${\tilde{⋄}}^{'}$ is an extension of $⋄^{'}$ , and ${\tilde{S}}^{'}$ is an extension of $S^{'}$ . (No constraint is imposed on the final components $\tilde{I}, I$ .) This is a preordering.

LaTeX Lean