Logiweb codex of peano

Up Help

peano, intro(∗, ∗, ∗, ∗), intro(∗, ∗, ∗), ˙0, ˙1, ˙2, ȧ, ḃ, ċ, ḋ, ė, ḟ, ġ, ḣ, i̇, j̇, k̇, l̇, ṁ, ṅ, ȯ, ṗ, q̇, ṙ, ṡ, ṫ, u̇, v̇, ẇ, ẋ, ẏ, ż, ṅonfree(∗, ∗), ṅonfree^{∗}(∗, ∗), ḟree⟨∗|∗ := ∗⟩, ḟree^{∗}⟨∗|∗ := ∗⟩, ∗≡⟨∗|∗ := ∗⟩, ∗≡⟨^{∗}∗|∗ := ∗⟩, S, A1, A2, A3, A4, A5, S1, S2, S3, S4, S5, S6, S7, S8, S9, MP, Gen, L3.2(a), ˙∗, ∗′, ∗ ˙· ∗, ∗ ˙+ ∗, ∗ =^{p} ∗, ∗^{P}, ˙¬ ∗,

∗ ˙∧ ∗, ∗ ˙∨ ∗, ˙∀∗: ∗, ˙∃∗: ∗, ∗ ˙⇒ ∗, ∗ ˙⇔ ∗,

peano

[peano →^{prio} Preassociative [peano], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [math ∗ end math], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)],

[S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)], [S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)],

[S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)], [S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [˙0], [˙1], [˙2], [ȧ], [ḃ], [ċ], [ḋ], [ė], [ḟ], [ġ], [ḣ], [i̇], [j̇], [k̇], [l̇], [ṁ], [ṅ], [ȯ], [ṗ], [q̇], [ṙ], [ṡ], [ṫ], [u̇], [v̇], [ẇ], [ẋ], [ẏ], [ż], [ṅonfree(∗, ∗)], [ṅonfree^{∗}(∗, ∗)], [ḟree⟨∗|∗ := ∗⟩], [ḟree^{∗}⟨∗|∗ := ∗⟩], [∗≡⟨∗|∗ := ∗⟩], [∗≡⟨^{∗}∗|∗ := ∗⟩], [S], [A1], [A2], [A3], [A4], [A5], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [MP], [Gen], [L3.2(a)]; Preassociative [∗ {∗}], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [˙∗]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], [”∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗]; Preassociative [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}], [∗′]; Preassociative [∗ · ∗], [∗ ·_{0} ∗], [∗ ˙· ∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗], [∗ ˙+ ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗],

[∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ =^{p} ∗], [∗^{P}];

Preassociative [¬∗], [ ˙¬ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗], [∗ ˙∨ ∗]; Preassociative [ ˙∀∗: ∗], [ ˙∃∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ˙⇒ ∗], [∗ ˙⇔ ∗]; Postassociative [∗ : ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗]; Postassociative [∗ then ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗]; ]

[peano →^{pyk} “peano”]

intro(∗, ∗, ∗, ∗)

[intro(x, i, p, t) →^{name} “ intro(#1. , #2. , #3. , #4. )”]

[intro(x, i, p, t) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[intro(x, i, p, t) ¨= [x =^{pyk} p][x =^{tex} t]]⌉)]

[intro(x, i, p, t) →^{tex} “\index{#2.: #3. @#2.: $[#1/tex name/tex.]$ #3.}% \index{#3. $[#1/tex name/tex.]$}% \tex{ $[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #4/tex name. ]$}$[ #1/tex name/tex.% ]$\footnote{$[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #3/tex name. ]$}”]

[intro(x, i, p, t) →^{pyk} “intro ∗ index ∗ pyk ∗ tex ∗ end intro”]

intro(∗, ∗, ∗)

[intro(x, p, t) →^{name} “ intro(#1. , #2. , #3. )”]

[intro(x, p, t) →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[intro(x, p, t) ¨= [x =^{pyk} p][x =^{tex} t]]⌉)]

[intro(x, p, t) →^{tex} “\index{\alpha #2. @\back \makebox[20mm][l]{$[#1/tex name/tex.]$}#2.}% \index{#2. $[#1/tex name/tex.]$}% \tex{ $[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #3/tex name. ]$}$[ #1/tex name/tex.% ]$\footnote{$[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #2/tex name. ]$}”]

[intro(x, p, t) →^{pyk} “intro ∗ pyk ∗ tex ∗ end intro”]

˙0

[˙0 →^{tex} “

\dot{0}”]

[˙0 →^{pyk} “peano zero”]

˙1

[˙1 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[˙1 ¨= ˙0′]⌉)]

[˙1 →^{tex} “

\dot{1}”]

[˙1 →^{pyk} “peano one”]

˙2

[˙2 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[˙2 ¨= ˙1′]⌉)]

[˙2 →^{tex} “

\dot{2}”]

[˙2 →^{pyk} “peano two”]

ȧ

[ȧ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ȧ ¨= ȧ]⌉)]

[ȧ →^{tex} “

\dot{\mathit{a}}”] [ȧ →^{pyk} “peano a”]

ḃ

[ḃ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḃ ¨= ḃ]⌉)]

[ḃ →^{tex} “

\dot{\mathit{b}}”] [ḃ →^{pyk} “peano b”]

ċ

[ċ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ċ ¨= ċ]⌉)]

[ċ →^{tex} “

\dot{\mathit{c}}”] [ċ →^{pyk} “peano c”]

ḋ

[ḋ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḋ ¨= ḋ]⌉)]

[ḋ →^{tex} “

\dot{\mathit{d}}”] [ḋ →^{pyk} “peano d”]

ė

[ė →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ė ¨= ė]⌉)]

[ė →^{tex} “

\dot{\mathit{e}}”] [ė →^{pyk} “peano e”]

ḟ

[ḟ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḟ ¨= ḟ]⌉)]

[ḟ →^{tex} “

\dot{\mathit{f}}”]

[ḟ →^{pyk} “peano f”]

ġ

[ġ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ġ ¨= ġ]⌉)]

[ġ →^{tex} “

\dot{\mathit{g}}”]

[ġ →^{pyk} “peano g”]

ḣ

[ḣ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḣ ¨= ḣ]⌉)]

[ḣ →^{tex} “

\dot{\mathit{h}}”]

[ḣ →^{pyk} “peano h”]

i̇

[i̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[i̇ ¨= i̇]⌉)]

[i̇ →^{tex} “

\dot{\mathit{i}}”]

[i̇ →^{pyk} “peano i”]

j̇

[j̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[j̇ ¨= j̇]⌉)]

[j̇ →^{tex} “

\dot{\mathit{j}}”]

[j̇ →^{pyk} “peano j”]

k̇

[k̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[k̇ ¨= k̇]⌉)]

[k̇ →^{tex} “

\dot{\mathit{k}}”] [k̇ →^{pyk} “peano k”]

l̇

[l̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[l̇ ¨= l̇]⌉)]

[l̇ →^{tex} “

\dot{\mathit{l}}”] [l̇ →^{pyk} “peano l”]

ṁ

[ṁ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṁ ¨= ṁ]⌉)]

[ṁ →^{tex} “

\dot{\mathit{m}}”] [ṁ →^{pyk} “peano m”]

ṅ

[ṅ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṅ ¨= ṅ]⌉)]

[ṅ →^{tex} “

\dot{\mathit{n}}”] [ṅ →^{pyk} “peano n”]

ȯ

[ȯ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ȯ ¨= ȯ]⌉)]

[ȯ →^{tex} “

\dot{\mathit{o}}”] [ȯ →^{pyk} “peano o”]

ṗ

[ṗ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṗ ¨= ṗ]⌉)]

[ṗ →^{tex} “

\dot{\mathit{p}}”] [ṗ →^{pyk} “peano p”]

q̇

[q̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[q̇ ¨= q̇]⌉)]

[q̇ →^{tex} “

\dot{\mathit{q}}”] [q̇ →^{pyk} “peano q”]

ṙ

[ṙ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṙ ¨= ṙ]⌉)]

[ṙ →^{tex} “

\dot{\mathit{r}}”] [ṙ →^{pyk} “peano r”]

ṡ

[ṡ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṡ ¨= ṡ]⌉)]

[ṡ →^{tex} “

\dot{\mathit{s}}”] [ṡ →^{pyk} “peano s”]

ṫ

[ṫ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṫ ¨= ṫ]⌉)]

[ṫ →^{tex} “

\dot{\mathit{t}}”] [ṫ →^{pyk} “peano t”]

u̇

[u̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[u̇ ¨= u̇]⌉)]

[u̇ →^{tex} “

\dot{\mathit{u}}”] [u̇ →^{pyk} “peano u”]

v̇

[v̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[v̇ ¨= v̇]⌉)]

[v̇ →^{tex} “

\dot{\mathit{v}}”] [v̇ →^{pyk} “peano v”]

ẇ

[ẇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẇ ¨= ẇ]⌉)]

[ẇ →^{tex} “

\dot{\mathit{w}}”] [ẇ →^{pyk} “peano w”]

ẋ

[ẋ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẋ ¨= ẋ]⌉)]

[ẋ →^{tex} “

\dot{\mathit{x}}”] [ẋ →^{pyk} “peano x”]

ẏ

[ẏ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẏ ¨= ẏ]⌉)]

[ẏ →^{tex} “

\dot{\mathit{y}}”] [ẏ →^{pyk} “peano y”]

ż

[ż →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ż ¨= ż]⌉)]

[ż →^{tex} “

\dot{\mathit{z}}”]

[ż →^{pyk} “peano z”]

ṅonfree(∗, ∗)

[ṅonfree(x, y) →^{val}

If(y^{P}, ¬ [ x =^{t} y ] ,

If(¬ [ y =^{r} ⌈ ˙∀x: y⌉ ] , ṅonfree^{∗}(x, y^{t}), If(x =^{t} [ y^{1} ] , T, ṅonfree(x, y^{2}))))]

[ṅonfree(x, y) →^{tex} “ \dot{nonfree}(#1. , #2. )”]

[ṅonfree(x, y) →^{pyk} “peano nonfree ∗ in ∗ end nonfree”]

ṅonfree^{∗}(∗, ∗)

[ṅonfree^{∗}(x, y) →^{val} x!If(y, T, If(ṅonfree(x, y^{h}), ṅonfree^{∗}(x, y^{t}), F))]

[ṅonfree^{∗}(x, y) →^{tex} “ \dot{nonfree}ˆ ∗(#1. , #2. )”]

[ṅonfree^{∗}(x, y) →^{pyk} “peano nonfree star ∗ in ∗ end nonfree”]

ḟree⟨∗|∗ := ∗⟩

[ḟree⟨a|x := b⟩ →^{val} x! [ b! If(a^{P}, T, If(¬ [ a =^{r} ⌈ ˙∀u: v⌉ ] , ḟree^{∗}⟨a^{t}|x := b⟩,

If(a^{1} =^{t} x, T,

If(ṅonfree(x, a^{2}), T, If(¬ṅonfree(a^{1}, b), F, ḟree⟨a^{2}|x := b⟩))))) ] ]

[ḟree⟨a|x := b⟩ →^{tex} “ \dot{free}\langle #1. | #2. := #3. \rangle”]

[ḟree⟨a|x := b⟩ →^{pyk} “peano free ∗ set ∗ to ∗ end free”]

ḟree^{∗}⟨∗|∗ := ∗⟩

[ḟree^{∗}⟨a|x := b⟩ →^{val} x! [ b!If(a, T, If(ḟree⟨a^{h}|x := b⟩, ḟree^{∗}⟨a^{t}|x := b⟩, F)) ] ]

[ḟree^{∗}⟨a|x := b⟩ →^{tex} “ \dot{free}{}ˆ ∗\langle #1. | #2. := #3. \rangle”]

[ḟree^{∗}⟨a|x := b⟩ →^{pyk} “peano free star ∗ set ∗ to ∗ end free”]

∗≡⟨∗|∗ := ∗⟩

[a≡⟨b|x := c⟩ →^{val} a! [ x! [ c! If(If(b =^{r} ⌈ ˙∀u: v⌉, b^{1} =^{t} x, F), a =^{t} b, If(b^{P} ∧ [ b =^{t} x ] , a =^{t} c, If( [ a ] =^{r} b, a^{t}≡⟨^{∗}b^{t}|x := c⟩, F))) ] ] ]

[a≡⟨b|x := c⟩ →^{tex} “#1.

{\equiv}\langle #2. |#3. :=#4. \rangle”]

[a≡⟨b|x := c⟩ →^{pyk} “peano sub ∗ is ∗ where ∗ is ∗ end sub”]

∗≡⟨^{∗}∗|∗ := ∗⟩

[a≡⟨^{∗}b|x := c⟩ →^{val} b! [ x! [ c!If(a, T, If(a^{h}≡⟨b^{h}|x := c⟩, a^{t}≡⟨^{∗}b^{t}|x := c⟩, F)) ] ] ]

[a≡⟨^{∗}b|x := c⟩ →^{tex} “#1.

{\equiv}\langleˆ ∗ #2. |#3. :=#4. \rangle”]

[a≡⟨^{∗}b|x := c⟩ →^{pyk} “peano sub star ∗ is ∗ where ∗ is ∗ end sub”]

S

[S →^{stmt} [ [ ȧ′ =^{p} [ ḃ′ ] ] ˙⇒ [ ȧ =^{p} [ ḃ ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ] ⊕ [ [ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: [ ṅonfree(\underline{x}, \underline{a}) ⊢⊢ [ [ ˙∀\underline{x}: [ \underline{a} ˙⇒ \underline{b} ] ] ˙⇒ [ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b} ] ] ] ]

⊕ [ [ [ ȧ ˙· [ ḃ′ ] ] =^{p} [ [ ȧ ˙· [ ḃ ] ] ˙+ [ ȧ ] ] ] ⊕ [ [ [ ȧ =^{p} [ ḃ ] ] ˙⇒ [ ȧ′ =^{p}

[ ḃ′ ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} ˙⇒ \underline{b} ] ⊢ [ \underline{a} ⊢ \underline{b} ] ] ] ⊕ [ [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ]

˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ⊕ [ [ [ ȧ ˙+ [ ḃ′ ] ] =^{p} [ [ ȧ ˙+ [ ḃ ] ] ′ ] ] ⊕ [

[ ¬ [ ˙0 =^{p} [ ȧ′ ] ] ] ⊕ [ [ ∀\underline{x}: ∀\underline{a}: [ \underline{a} ⊢ ˙∀\underline{x}: \underline{a} ] ] ⊕ [ [ ∀\underline{c}: ∀\underline{x}: ∀\underline{b}: ∀\underline{a}: [ \underline{a}≡⟨\underline{b}|\underline{x} := \underline{c}⟩ ⊢⊢ [ [ ˙∀\underline{x}: \underline{b} ] ˙⇒ \underline{a} ] ] ] ⊕ [ [ [ ȧ ˙· ˙0 ] =^{p} ˙0 ] ⊕ [ [ [ ȧ =^{p} [ ḃ ] ] ˙⇒ [ [ ȧ =^{p} [ ċ ] ] ˙⇒ [ ḃ =^{p} [ ċ ] ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{x}: [ \underline{b}≡⟨\underline{a}|\underline{x} := ˙0⟩ ⊢⊢ [ \underline{c}≡⟨\underline{a}|\underline{x} := \underline{x}′⟩ ⊢⊢ [ \underline{b} ˙⇒ [ [ ˙∀\underline{x}: [ \underline{a} ˙⇒ \underline{c} ] ] ˙⇒ ˙∀\underline{x}: \underline{a} ] ] ] ] ] ⊕ [ [ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}:

[ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ] ⊕ [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ]

] ] ] ] ] ] ] ] ] ] ] ] ] ] ] ]

[S →^{tex} “

S”]

[S →^{pyk} “system s”]

A1

[A1 →^{proof} Rule tactic]

[A1 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{a} ] ] ]

[A1 →^{tex} “

A1”]

[A1 →^{pyk} “axiom a one”]

A2

[A2 →^{proof} Rule tactic]

[A2 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: [ [ \underline{a} ˙⇒ [ \underline{b} ˙⇒ \underline{c} ] ] ˙⇒ [ [ \underline{a} ˙⇒ \underline{b} ] ˙⇒ [ \underline{a} ˙⇒ \underline{c} ] ] ] ]

[A2 →^{tex} “

A2”] [A2 →^{pyk} “axiom a two”]

A3

[A3 →^{proof} Rule tactic] [A3 →^{stmt} S ⊢ [ [ [ ˙¬ \underline{b} ] ˙⇒ ˙¬ \underline{a} ] ˙⇒ [ [ [ ˙¬ \underline{b} ] ˙⇒ \underline{a} ] ˙⇒ \underline{b} ] ] ]

[A3 →^{tex} “

A3”] [A3 →^{pyk} “axiom a three”]

A4

[A4 →^{proof} Rule tactic] [A4 →^{stmt} S ⊢ ∀\underline{c}: ∀\underline{x}: ∀\underline{b}: ∀\underline{a}: [ \underline{a}≡⟨\underline{b}|\underline{x} := \underline{c}⟩ ⊢⊢ [ [ ˙∀\underline{x}: \underline{b} ] ˙⇒ \underline{a} ] ] ]

[A4 →^{tex} “

A4”] [A4 →^{pyk} “axiom a four”]

A5

[A5 →^{proof} Rule tactic] [A5 →^{stmt} S ⊢ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: [ ṅonfree(\underline{x}, \underline{a}) ⊢⊢ [ [ ˙∀\underline{x}: [ \underline{a} ˙⇒ \underline{b} ] ] ˙⇒ [ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b} ] ] ] ]

[A5 →^{tex} “

A5”] [A5 →^{pyk} “axiom a five”]

S1

[S1 →^{proof} Rule tactic] [S1 →^{stmt} S ⊢ [ [ ȧ =^{p} [ ḃ ] ] ˙⇒ [ [ ȧ =^{p} [ ċ ] ] ˙⇒ [ ḃ =^{p} [ ċ ] ] ] ] ]

[S1 →^{tex} “

S1”] [S1 →^{pyk} “axiom s one”]

S2

[S2 →^{proof} Rule tactic] [S2 →^{stmt} S ⊢ [ [ ȧ =^{p} [ ḃ ] ] ˙⇒ [ ȧ′ =^{p} [ ḃ′ ] ] ] ]

[S2 →^{tex} “

S2”] [S2 →^{pyk} “axiom s two”]

S3

[S3 →^{proof} Rule tactic] [S3 →^{stmt} S ⊢ ¬ [ ˙0 =^{p} [ ȧ′ ] ] ]

[S3 →^{tex} “

S3”] [S3 →^{pyk} “axiom s three”]

S4

[S4 →^{proof} Rule tactic] [S4 →^{stmt} S ⊢ [ [ ȧ′ =^{p} [ ḃ′ ] ] ˙⇒ [ ȧ =^{p} [ ḃ ] ] ] ]

[S4 →^{tex} “

S4”] [S4 →^{pyk} “axiom s four”]

S5

[S5 →^{proof} Rule tactic] [S5 →^{stmt} S ⊢ [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ] ] ]

[S5 →^{tex} “

S5”] [S5 →^{pyk} “axiom s five”]

S6

[S6 →^{proof} Rule tactic] [S6 →^{stmt} S ⊢ [ [ ȧ ˙+ [ ḃ′ ] ] =^{p} [ [ ȧ ˙+ [ ḃ ] ] ′ ] ] ]

[S6 →^{tex} “

S6”] [S6 →^{pyk} “axiom s six”]

S7

[S7 →^{proof} Rule tactic] [S7 →^{stmt} S ⊢ [ [ ȧ ˙· ˙0 ] =^{p} ˙0 ] ]

[S7 →^{tex} “

S7”] [S7 →^{pyk} “axiom s seven”]

S8

[S8 →^{proof} Rule tactic] [S8 →^{stmt} S ⊢ [ [ ȧ ˙· [ ḃ′ ] ] =^{p} [ [ ȧ ˙· [ ḃ ] ] ˙+ [ ȧ ] ] ] ]

[S8 →^{tex} “

S8”] [S8 →^{pyk} “axiom s eight”]

S9

[S9 →^{proof} Rule tactic] [S9 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{x}: [ \underline{b}≡⟨\underline{a}|\underline{x} := ˙0⟩ ⊢⊢ [ \underline{c}≡⟨\underline{a}|\underline{x} := \underline{x}′⟩ ⊢⊢ [ \underline{b} ˙⇒ [ [ ˙∀\underline{x}: [ \underline{a} ˙⇒ \underline{c} ] ] ˙⇒ ˙∀\underline{x}: \underline{a} ] ] ] ] ]

[S9 →^{tex} “

S9”] [S9 →^{pyk} “axiom s nine”]

MP

[MP →^{proof} Rule tactic] [MP →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: [ [ \underline{a} ˙⇒ \underline{b} ] ⊢ [ \underline{a} ⊢ \underline{b} ] ] ]

[MP →^{tex} “

MP”] [MP →^{pyk} “rule mp”]

Gen

[Gen →^{proof} Rule tactic] [Gen →^{stmt} S ⊢ ∀\underline{x}: ∀\underline{a}: [ \underline{a} ⊢ ˙∀\underline{x}: \underline{a} ] ]

[Gen →^{tex} “

Gen”] [Gen →^{pyk} “rule gen”]

L3.2(a)

[L3.2(a) →^{proof} λc.λx.P(⌈S ⊢ [ [ S5 ≫ [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ] ] ] ; [ [ [ Gen ⊳ [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ] ] ] ≫ ˙∀ȧ: [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ] ] ] ; [ [ [ [ [ [ A4 @ [ ẋ ] ] @ [ ȧ ] ] @ [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ] ] ] @ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ≫ [ [ ˙∀ȧ: [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ] ] ] ˙⇒ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ] ; [ [ [ MP ⊳ [ [ ˙∀ȧ: [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ] ] ] ˙⇒ [ [ ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ] ⊳ ˙∀ȧ: [ [ ȧ ˙+ ˙0 ] =^{p} [ ȧ ] ] ] ≫ [ [

ẋ ˙+ ˙0 ] =^{p} [ ẋ ] ] ] ] ] ] ⌉, p_{0}, c)]

[L3.2(a) →^{stmt} S ⊢ [ ẋ =^{p} [ ẋ ] ] ]

[L3.2(a) →^{tex} “

L3.2(a)”] [L3.2(a) →^{pyk} “lemma l three two a”]

˙∗

[ẋ →^{tex} “

\dot{#1. }”]

[ẋ →^{pyk} “∗ peano var”]

∗′

[x′ →^{tex} “#1.

’”]

[x′ →^{pyk} “∗ peano succ”]

∗ ˙· ∗

[x ˙· y →^{tex} “#1.

\mathop{\dot{\cdot}} #2.”]

[x ˙· y →^{pyk} “∗ peano times ∗”]

∗ ˙+ ∗

[x ˙+ y →^{tex} “#1.

\mathop{\dot{+}} #2.”]

[x ˙+ y →^{pyk} “∗ peano plus ∗”]

∗ =^{p} ∗

[x =^{p} y →^{tex} “#1.

\stackrel{p}{=} #2.”]

[x =^{p} y →^{pyk} “∗ peano is ∗”]

∗^{P}

[x^{P} →^{val} x =^{r} ⌈ẋ⌉]

[x^{P} →^{tex} “#1.

{} ˆ {\cal P}”]

[x^{P} →^{pyk} “∗ is peano var”]

˙¬ ∗

[ ˙¬ x →^{tex} “

\dot{\neg}\, #1.”]

[ ˙¬ x →^{pyk} “peano not ∗”]

∗ ˙∧ ∗

[x ˙∧ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙∧ y ¨= ˙¬ (x ˙⇒ ˙¬ y)]⌉)]

[x ˙∧ y →^{tex} “#1.

\mathrel{\dot{\wedge}} #2.”]

[x ˙∧ y →^{pyk} “∗ peano and ∗”]

∗ ˙∨ ∗

[x ˙∨ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙∨ y ¨= [ ˙¬ x ] ˙⇒ y]⌉)]

[x ˙∨ y →^{tex} “#1.

\mathrel{\dot{\vee}} #2.”]

[x ˙∨ y →^{pyk} “∗ peano or ∗”]

˙∀∗: ∗

[ ˙∀x: y →^{tex} “

\dot{\forall} #1. \colon #2.”]

[ ˙∀x: y →^{pyk} “peano all ∗ indeed ∗”]

˙∃∗: ∗

[ ˙∃x: y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ ˙∃x: y ¨= ˙¬ ˙∀x: ˙¬ y]⌉)]

[ ˙∃x: y →^{tex} “

\dot{\exists} #1. \colon #2.”]

[ ˙∃x: y →^{pyk} “peano exist ∗ indeed ∗”]

∗ ˙⇒ ∗

[x ˙⇒ y →^{tex} “#1.

\mathrel{\dot{\Rightarrow}} #2.”]

[x ˙⇒ y →^{pyk} “∗ peano imply ∗”]

∗ ˙⇔ ∗

[x ˙⇔ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙⇔ y ¨= (x ˙⇒ y) ˙∧ (y ˙⇒ x)]⌉)]

[x ˙⇔ y →^{tex} “#1.

\mathrel{\dot{\Leftrightarrow}} #2.”]

[x ˙⇔ y →^{pyk} “∗ peano iff ∗”]

The pyk compiler, version 0.grue.20050502+ by Klaus Grue GRD-2005-06-02.UTC:10:16:52.703168 = MJD-53523.TAI:10:17:24.703168 = LGT-4624424244703168e-6