Logiweb codex of problemtwo

Up Help

∗ ⇒ ∗, problemtwo, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, L_{o}, pred calc, pc1, pc2, pc3, pc4, pc5, pc6, pc7, pc8, pc9, pc10, pc11, pc12, pcmp, pcunsound, pcded, pcia, pcie, pcdeduction, trivia, trivia2, iatest, andintro, andelim1, andelim2, orintro1, orintro2, orelim, notintro, notnotintro, notnotelim, mt, pbc, repeat, lem, forallintro, forallelim, existsintro, existselim, bottomelim, lemnotintro, nontriv0, nontriv1, nontriv2, nontriv3, nontriv4, nontriv5, nontriv6, ∗ ≡ ∗, ∗ = ∗, ¬∗, ∗ ∧ ∗, ∗ ∨ ∗, ∀ ∗ . (∗), ∃ ∗ . (∗), ∗ ∈ ∗,

∗ ⇒ ∗

[x ⇒ y →^{tex} “#1. \Rightarrow #2.”]

problemtwo

[problemtwo →^{prio} Preassociative [problemtwo], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [ $ ∗ $ ], [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̃^{∗}(∗, ∗, ∗)], [(∗)], [(∗)], [display(∗)], [statement(∗)], [[∗]^{·}], [[∗]^{−}], [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}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [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}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [L_{o}], [check], [[∗ =^{∘} ∗]], [RootVisible(∗)], [A], [R], [C], [T], [L], [\{∗\}], [\overline{∗}], [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], [⟨∗≡ ∗ | ∗:=∗⟩], [⟨∗≡^{0} ∗ | ∗:=∗⟩], [⟨∗≡^{1} ∗ | ∗:=∗⟩], [⟨∗≡^{∗} ∗ | ∗:=∗⟩], [Ded(∗, ∗)], [Ded_{0}(∗, ∗)], [Ded_{1}(∗, ∗, ∗)], [Ded_{2}(∗, ∗, ∗)], [Ded_{3}(∗, ∗, ∗, ∗)], [Ded_{4}(∗, ∗, ∗, ∗)], [Ded_{4}^{∗}(∗, ∗, ∗, ∗)], [Ded_{5}(∗, ∗, ∗)], [Ded_{6}(∗, ∗, ∗, ∗)], [Ded_{6}^{∗}(∗, ∗, ∗, ∗)], [Ded_{7}(∗)], [Ded_{8}(∗, ∗)], [Ded_{8}^{∗}(∗, ∗)], [S], [Neg], [MP], [Gen], [Ded], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [Repetition], [A1′], [A2′], [A4′], [A5′], [Prop 3.2a], [Prop 3.2b], [Prop 3.2c], [Prop 3.2d], [Prop 3.2e_{1}], [Prop 3.2e_{2}], [Prop 3.2e], [Prop 3.2f_{1}], [Prop 3.2f_{2}], [Prop 3.2f], [Prop 3.2g_{1}], [Prop 3.2g_{2}], [Prop 3.2g], [Prop 3.2h_{1}], [Prop 3.2h_{2}], [Prop 3.2h], [Block_{1}(∗, ∗, ∗)], [Block_{2}(∗)], [pred calc], [pc1], [pc2], [pc3], [pc4], [pc5], [pc6], [pc7], [pc8], [pc9], [pc10], [pc11], [pc12], [pcmp], [pcunsound], [pcded], [pcia], [pcie], [pcdeduction], [trivia], [trivia2], [iatest], [andintro], [andelim1], [andelim2], [orintro1], [orintro2], [orelim], [notintro], [notnotintro], [notnotelim], [mt], [pbc], [repeat], [lem], [forallintro], [forallelim], [existsintro], [existselim], [bottomelim], [lemnotintro], [nontriv0], [nontriv1], [nontriv2], [nontriv3], [nontriv4], [nontriv5], [nontriv6]; Preassociative [∗ {∗}], [∗/indexintro(∗, ∗, ∗, ∗)], [∗/intro(∗, ∗, ∗)], [∗/bothintro(∗, ∗, ∗, ∗, ∗)], [∗/nameintro(∗, ∗, ∗, ∗)], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)], [∗^{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^{∗}}], [∗^{hide}]; 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 ∗], [MacroIndent(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗′]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; 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} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ = ∗], [∗ ≠ ∗], [∗^{var}], [∗#^{0}∗], [∗#^{1}∗], [∗#^{∗}∗], [∗ ≡ ∗], [∗ = ∗]; Preassociative [¬∗], [¬∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗], [∗ ∨ ∗]; Preassociative [∃∗: ∗], [∀∗: ∗], [∀_{obj}∗: ∗], [∀ ∗ . (∗)], [∃ ∗ . (∗)]; Postassociative [∗ ¨⇒ ∗], [∗ ⇒ ∗], [∗ ⇔ ∗]; Postassociative [∗ : ∗], [∗ spy ∗], [∗!∗]; Preassociative

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

Preassociative [λ ∗ .∗], [Λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗#∗]; 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 ≫ ∗ = ∗; ∗], [Begin ∗; ∗ : End; ∗], [Last block line ∗ ≫ ∗; ], [Arbitrary ≫ ∗; ∗]; Postassociative [∗ | ∗]; Postassociative [∗ , ∗], [∗[ ∗]∗]; Preassociative [∗&∗], [→]; Preassociative [∗\\∗], [∗ linebreak[4] ∗], [∗\\∗]; Preassociative [∗ ∈ ∗]; ]

[problemtwo →^{pyk} “problemtwo”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell aa”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell ab”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell ac”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”] [L_{o} →^{pyk} “ell ad”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell ae”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell af”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell ag”]

L_{o}

[L_{o} →^{tex} “

\xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 [L_{o} →^{pyk} “ell ah”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell ai”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell aj”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell ak”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell al”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell am”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell an”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”] [L_{o} →^{pyk} “ell ao”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell ap”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell aq”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 \xdef \lgwello {L\ifnum \lgwproofline <10 0\fi \number \lgwproofline } \fi \lgwello \fi ”]

[L_{o} →^{pyk} “ell ar”]

L_{o}

[L_{o} →^{tex} “

\if \relax \csname lgwprooflinep\endcsname L o \else \if \relax \csname lgwello\endcsname \global \advance \lgwproofline by 1 [L_{o} →^{pyk} “ell as”]

pred calc

[pred calc →^{stmt} ∀\underline{x}: ∀\underline{r}: ∀\underline{g}: ∀\underline{f}: ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊢⊢ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ⊢⊢

∀\underline{x}. (\underline{f}) ⇒ \underline{g} ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ⇒ \underline{f} ∧ \underline{g} ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ \underline{g} ⇒ \underline{g} ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{g} ⊢ \underline{f} ⇒ \underline{g} ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ⇒ \underline{f} ⇒ ¬\underline{g} ⇒ ¬\underline{f} ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ⇒ \underline{f} ⊕ ∀\underline{f}: ∀\underline{g}: ∀\underline{x}: ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ \underline{f} ⇒ \underline{g} ⊢ ∃\underline{x}. (\underline{f}) ⇒ \underline{g} ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ∨ \underline{f} ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{f} ⇒ \underline{g} ⊢ \underline{g} ⊕ ∀\underline{f}: ¬¬\underline{f} ⇒ \underline{f} ⊕ ∀\underline{f}: ∀\underline{g}: ∀\underline{h}: \underline{f} ⇒ \underline{g} ⇒ \underline{f} ⇒ \underline{g} ⇒ \underline{h} ⇒ \underline{f} ⇒ \underline{h} ⊕ ∀\underline{a}: ∀\underline{b}: λx.Ded_{0}(⌈\underline{a}⌉, ⌈\underline{b}⌉) ⊢⊢ \underline{a} ⊢ \underline{b} ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ \underline{g} ⇒ \underline{f} ⊕ ∀\underline{f}: ∀\underline{g}: ∀\underline{h}: \underline{f} ⇒ \underline{g} ⇒ \underline{h} ⇒ \underline{g} ⇒ \underline{f} ∨ \underline{h} ⇒ \underline{g} ⊕ ∀\underline{f}: ∀\underline{g}: ∀\underline{x}: ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ \underline{g} ⇒ \underline{f} ⊢ \underline{g} ⇒ ∀\underline{x}. (\underline{f}) ⊕ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{f} ∨ \underline{g} ⊕ ∀\underline{x}: ∀\underline{r}: ∀\underline{g}: ∀\underline{f}: ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊢⊢ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ⊢⊢ \underline{g} ⇒ ∃\underline{x}. (\underline{f})]

[pred calc →^{pyk} “pred calc”]

pc1

[pc1 →^{proof} Rule tactic]

[pc1 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ⇒ \underline{f}]

[pc1 →^{pyk} “pc1”]

pc2

[pc2 →^{proof} Rule tactic]

[pc2 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ∀\underline{h}: \underline{f} ⇒ \underline{g} ⇒ \underline{f} ⇒ \underline{g} ⇒ \underline{h} ⇒ \underline{f} ⇒ \underline{h}]

[pc2 →^{pyk} “pc2”]

pc3

[pc3 →^{proof} Rule tactic]

[pc3 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ⇒ \underline{f} ∧ \underline{g}]

[pc3 →^{pyk} “pc3”]

pc4

[pc4 →^{proof} Rule tactic] [pc4 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{f} ∨ \underline{g}]

[pc4 →^{pyk} “pc4”]

pc5

[pc5 →^{proof} Rule tactic] [pc5 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ∨ \underline{f}]

[pc5 →^{pyk} “pc5”]

pc6

[pc6 →^{proof} Rule tactic] [pc6 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ \underline{g} ⇒ \underline{f}]

[pc6 →^{pyk} “pc6”]

pc7

[pc7 →^{proof} Rule tactic] [pc7 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ \underline{g} ⇒ \underline{g}]

[pc7 →^{pyk} “pc7”]

pc8

[pc8 →^{proof} Rule tactic] [pc8 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ∀\underline{h}: \underline{f} ⇒ \underline{g} ⇒ \underline{h} ⇒ \underline{g} ⇒ \underline{f} ∨ \underline{h} ⇒ \underline{g}]

[pc8 →^{pyk} “pc8”]

pc9

[pc9 →^{proof} Rule tactic] [pc9 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ⇒ \underline{f} ⇒ ¬\underline{g} ⇒ ¬\underline{f}]

[pc9 →^{pyk} “pc9”]

pc10

[pc10 →^{proof} Rule tactic] [pc10 →^{stmt} pred calc ⊢ ∀\underline{f}: ¬¬\underline{f} ⇒ \underline{f}]

[pc10 →^{pyk} “pc10”]

pc11

[pc11 →^{proof} Rule tactic] [pc11 →^{stmt} pred calc ⊢ ∀\underline{x}: ∀\underline{r}: ∀\underline{g}: ∀\underline{f}: ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊢⊢ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ⊢⊢ ∀\underline{x}. (\underline{f}) ⇒ \underline{g}]

[pc11 →^{pyk} “pc11”]

pc12

[pc12 →^{proof} Rule tactic] [pc12 →^{stmt} pred calc ⊢ ∀\underline{x}: ∀\underline{r}: ∀\underline{g}: ∀\underline{f}: ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊢⊢ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ⊢⊢ \underline{g} ⇒ ∃\underline{x}. (\underline{f})]

[pc12 →^{pyk} “pc12”]

pcmp

[pcmp →^{proof} Rule tactic] [pcmp →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{f} ⇒ \underline{g} ⊢ \underline{g}] [pcmp →^{pyk} “pcmp”]

pcunsound

[pcunsound →^{pyk} “pcunsound”]

pcded

[pcded →^{proof} Rule tactic] [pcded →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{g} ⊢ \underline{f} ⇒ \underline{g}] [pcded →^{pyk} “pcded”]

pcia

[pcia →^{proof} Rule tactic] [pcia →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ∀\underline{x}: ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ \underline{g} ⇒ \underline{f} ⊢ \underline{g} ⇒ ∀\underline{x}. (\underline{f})] [pcia →^{pyk} “pcia”]

pcie

[pcie →^{proof} Rule tactic] [pcie →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ∀\underline{x}: ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ \underline{f} ⇒ \underline{g} ⊢ ∃\underline{x}. (\underline{f}) ⇒ \underline{g}] [pcie →^{pyk} “pcie”]

pcdeduction

[pcdeduction →^{proof} Rule tactic] [pcdeduction →^{stmt} pred calc ⊢ ∀\underline{a}: ∀\underline{b}: λx.Ded_{0}(⌈\underline{a}⌉, ⌈\underline{b}⌉) ⊢⊢ \underline{a} ⊢ \underline{b}] [pcdeduction →^{pyk} “pcdeduction”]

trivia

[trivia →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: pc2 ≫ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f}; pc1 ≫ \underline{f} ⇒ \underline{f} ⇒ \underline{f}; pcmp ⊳ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⊳ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ≫ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f}; pc1 ≫ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f}; pcmp ⊳ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⊳ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ⇒ \underline{f} ≫ \underline{f} ⇒ \underline{f}⌉, p_{0}, c)]

[trivia →^{stmt} pred calc ⊢ ∀\underline{f}: \underline{f} ⇒ \underline{f}]

[trivia →^{pyk} “trivia”]

trivia2

[trivia2 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{f}: \underline{f} ⊢ repeat ⊳ \underline{f} ≫ \underline{f}; pcdeduction ⊳ ∀\underline{f}: \underline{f} ⊢ \underline{f} ≫ \underline{f} ⊢ \underline{f}⌉, p_{0}, c)]

[trivia2 →^{stmt} pred calc ⊢ ∀\underline{f}: \underline{f} ⊢ \underline{f}]

[trivia2 →^{pyk} “trivia2”]

iatest

[iatest →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{g}: ∀\underline{y}: ⌈\underline{y}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ pc1 ≫ \underline{g} ⇒ \underline{y} ⇒ \underline{g}; pcia ⊳ ⊳ ⌈\underline{y}⌉#^{0}⌈\underline{g}⌉ ⊳ \underline{g} ⇒ \underline{y} ⇒ \underline{g} ≫ \underline{g} ⇒ ∀\underline{y}. (\underline{y} ⇒ \underline{g})⌉, p_{0}, c)]

[iatest →^{stmt} pred calc ⊢ ∀\underline{g}: ∀\underline{y}: ⌈\underline{y}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ \underline{g} ⇒ ∀\underline{y}. (\underline{y} ⇒ \underline{g})]

[iatest →^{pyk} “iatest”]

andintro

[andintro →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{g} ⊢ pc3 ≫ \underline{f} ⇒ \underline{g} ⇒ \underline{f} ∧\underline{g}; pcmp⊳\underline{f} ⊳\underline{f} ⇒ \underline{g} ⇒ \underline{f} ∧\underline{g} ≫ \underline{g} ⇒ \underline{f} ∧\underline{g}; pcmp⊳\underline{g} ⊳\underline{g} ⇒ \underline{f} ∧\underline{g} ≫ \underline{f} ∧\underline{g}⌉, p_{0}, c)]

[andintro →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{g} ⊢ \underline{f} ∧ \underline{g}]

[andintro →^{pyk} “andintro”]

andelim1

[andelim1 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ \underline{g} ⊢ pc6 ≫ \underline{f} ∧ \underline{g} ⇒ \underline{f}; pcmp ⊳ \underline{f} ∧ \underline{g} ⊳ \underline{f} ∧ \underline{g} ⇒ \underline{f} ≫ \underline{f}⌉, p_{0}, c)]

[andelim1 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ \underline{g} ⊢ \underline{f}]

[andelim1 →^{pyk} “andelim1”]

andelim2

[andelim2 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ \underline{g} ⊢ pc7 ≫ \underline{f} ∧ \underline{g} ⇒ \underline{g}; pcmp ⊳ \underline{f} ∧ \underline{g} ⊳ \underline{f} ∧ \underline{g} ⇒ \underline{g} ≫ \underline{g}⌉, p_{0}, c)]

[andelim2 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ \underline{g} ⊢ \underline{g}]

[andelim2 →^{pyk} “andelim2”]

orintro1

[orintro1 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ pc4 ≫ \underline{f} ⇒ \underline{f} ∨ \underline{g}; pcmp ⊳ \underline{f} ⊳ \underline{f} ⇒ \underline{f} ∨ \underline{g} ≫ \underline{f} ∨ \underline{g}⌉, p_{0}, c)]

[orintro1 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{f} ∨ \underline{g}]

[orintro1 →^{pyk} “orintro1”]

orintro2

[orintro2 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{g} ⊢ pc5 ≫ \underline{g} ⇒ \underline{f} ∨ \underline{g}; pcmp ⊳ \underline{g} ⊳ \underline{g} ⇒ \underline{f} ∨ \underline{g} ≫ \underline{f} ∨ \underline{g}⌉, p_{0}, c)]

[orintro2 →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{g} ⊢ \underline{f} ∨ \underline{g}]

[orintro2 →^{pyk} “orintro2”]

orelim

[orelim →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ∀\underline{h}: \underline{f} ∨ \underline{g} ⊢ \underline{f} ⊢ \underline{h} ⊢ \underline{g} ⊢ \underline{h} ⊢ pcded ⊳ \underline{f} ⊢ \underline{h} ≫ \underline{f} ⇒ \underline{h}; pcded ⊳ \underline{g} ⊢ \underline{h} ≫ \underline{g} ⇒ \underline{h}; pc8 ≫ \underline{f} ⇒ \underline{h} ⇒ \underline{g} ⇒ \underline{h} ⇒ \underline{f} ∨ \underline{g} ⇒ \underline{h}; pcmp⊳\underline{f} ⇒ \underline{h}⊳\underline{f} ⇒ \underline{h} ⇒ \underline{g} ⇒ \underline{h} ⇒ \underline{f}∨\underline{g} ⇒ \underline{h} ≫ \underline{g} ⇒ \underline{h} ⇒ \underline{f}∨\underline{g} ⇒ \underline{h}; pcmp⊳\underline{g} ⇒ \underline{h} ⊳ \underline{g} ⇒ \underline{h} ⇒ \underline{f} ∨ \underline{g} ⇒ \underline{h} ≫ \underline{f} ∨ \underline{g} ⇒ \underline{h}; pcmp ⊳ \underline{f} ∨ \underline{g} ⊳ \underline{f} ∨ \underline{g} ⇒ \underline{h} ≫ \underline{h}⌉, p_{0}, c)]

[orelim →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ∀\underline{h}: \underline{f} ∨ \underline{g} ⊢ \underline{f} ⊢ \underline{h} ⊢ \underline{g} ⊢ \underline{h} ⊢ \underline{h}]

[orelim →^{pyk} “orelim”]

notintro

[notintro →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{g} ⊢ \underline{f} ⊢ ¬\underline{g} ⊢ pcded ⊳ \underline{f} ⊢ \underline{g} ≫ \underline{f} ⇒ \underline{g}; pcded ⊳ \underline{f} ⊢ ¬\underline{g} ≫ \underline{f} ⇒ ¬\underline{g}; pc9 ≫ \underline{f} ⇒ \underline{g} ⇒ \underline{f} ⇒ ¬\underline{g} ⇒ ¬\underline{f}; pcmp ⊳ \underline{f} ⇒ \underline{g} ⊳ \underline{f} ⇒ \underline{g} ⇒ \underline{f} ⇒ ¬\underline{g} ⇒ ¬\underline{f} ≫ \underline{f} ⇒ ¬\underline{g} ⇒ ¬\underline{f}; pcmp⊳\underline{f} ⇒ ¬\underline{g}⊳\underline{f} ⇒ ¬\underline{g} ⇒ ¬\underline{f} ≫ ¬\underline{f}⌉, p_{0}, c)]

[notintro →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{g} ⊢ \underline{f} ⊢ ¬\underline{g} ⊢ ¬\underline{f}]

[notintro →^{pyk} “notintro”]

notnotintro

[notnotintro →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: \underline{f} ⊢ ∀\underline{f}: \underline{f} ⊢ ¬\underline{f} ⊢ repeat ⊳ \underline{f} ≫ \underline{f}; pcdeduction ⊳ ∀\underline{f}: \underline{f} ⊢ ¬\underline{f} ⊢ \underline{f} ≫ \underline{f} ⇒ ¬\underline{f} ⇒ \underline{f}; pcmp ⊳ \underline{f} ⊳ \underline{f} ⇒ ¬\underline{f} ⇒ \underline{f} ≫ ¬\underline{f} ⇒ \underline{f}; trivia ≫ ¬\underline{f} ⇒ ¬\underline{f}; pc9 ≫ ¬\underline{f} ⇒ \underline{f} ⇒ ¬\underline{f} ⇒ ¬\underline{f} ⇒ ¬¬\underline{f}; pcmp ⊳ ¬\underline{f} ⇒ \underline{f} ⊳ ¬\underline{f} ⇒ \underline{f} ⇒ ¬\underline{f} ⇒ ¬\underline{f} ⇒ ¬¬\underline{f} ≫ ¬\underline{f} ⇒ ¬\underline{f} ⇒ ¬¬\underline{f}; pcmp ⊳ ¬\underline{f} ⇒ ¬\underline{f} ⊳ ¬\underline{f} ⇒ ¬\underline{f} ⇒ ¬¬\underline{f} ≫ ¬¬\underline{f}⌉, p_{0}, c)]

[notnotintro →^{stmt} pred calc ⊢ ∀\underline{f}: \underline{f} ⊢ ¬¬\underline{f}]

[notnotintro →^{pyk} “notnotintro”]

notnotelim

[notnotelim →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ¬¬\underline{f} ⊢ pc10 ≫ ¬¬\underline{f} ⇒ \underline{f}; pcmp ⊳ ¬¬\underline{f} ⊳ ¬¬\underline{f} ⇒ \underline{f} ≫ \underline{f}⌉, p_{0}, c)]

[notnotelim →^{stmt} pred calc ⊢ ∀\underline{f}: ¬¬\underline{f} ⊢ \underline{f}]

[notnotelim →^{pyk} “notnotelim”]

mt

[mt →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ⊢ ¬\underline{g} ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ pcmp ⊳ \underline{f} ⊳ \underline{f} ⇒ \underline{g} ≫ \underline{g}; pcdeduction ⊳ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{g} ≫ \underline{f} ⊢ \underline{g}; ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ repeat ⊳ ¬\underline{g} ≫ ¬\underline{g}; pcdeduction⊳∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ ¬\underline{g} ≫ \underline{f} ⊢ ¬\underline{g}; notintro⊳\underline{f} ⊢ \underline{g}⊳\underline{f} ⊢ ¬\underline{g} ≫ ¬\underline{f}⌉, p_{0}, c)]

[mt →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ⊢ ¬\underline{g} ⊢ ¬\underline{f}]

[mt →^{pyk} “mt”]

pbc

[pbc →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ¬\underline{f} ⊢ \underline{g} ⊢ ¬\underline{f} ⊢ ¬\underline{g} ⊢ notintro ⊳ ¬\underline{f} ⊢ \underline{g} ⊳ ¬\underline{f} ⊢ ¬\underline{g} ≫ ¬¬\underline{f}; notnotelim ⊳ ¬¬\underline{f} ≫ \underline{f}⌉, p_{0}, c)]

[pbc →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ¬\underline{f} ⊢ \underline{g} ⊢ ¬\underline{f} ⊢ ¬\underline{g} ⊢ \underline{f}] [pbc →^{pyk} “pbc”]

repeat

[repeat →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: \underline{f} ⊢ trivia ≫ \underline{f} ⇒ \underline{f}; pcmp ⊳ \underline{f} ⊳ \underline{f} ⇒ \underline{f} ≫ \underline{f}⌉, p_{0}, c)]

[repeat →^{stmt} pred calc ⊢ ∀\underline{f}: \underline{f} ⊢ \underline{f}]

[repeat →^{pyk} “repeat”]

lem

[lem →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{f}: ¬\underline{f} ∨ ¬\underline{f} ⊢ ∀\underline{f}: \underline{f} ⊢ orintro1 ⊳ \underline{f} ≫ \underline{f} ∨ ¬\underline{f}; pcdeduction ⊳ ∀\underline{f}: \underline{f} ⊢ \underline{f} ∨ ¬\underline{f} ≫ \underline{f} ⊢ \underline{f} ∨ ¬\underline{f}; ∀\underline{f}: \underline{f} ⊢ repeat ⊳ ¬\underline{f} ∨ ¬\underline{f} ≫ ¬\underline{f} ∨ ¬\underline{f}; pcdeduction ⊳ ∀\underline{f}: \underline{f} ⊢ ¬\underline{f} ∨ ¬\underline{f} ≫ \underline{f} ⊢ ¬\underline{f} ∨ ¬\underline{f}; notintro ⊳ \underline{f} ⊢ \underline{f} ∨ ¬\underline{f} ⊳ \underline{f} ⊢ ¬\underline{f}∨¬\underline{f} ≫ ¬\underline{f}; orintro2⊳¬\underline{f} ≫ \underline{f}∨¬\underline{f}; pcdeduction⊳∀\underline{f}: ¬\underline{f}∨¬\underline{f} ⊢ \underline{f}∨¬\underline{f} ≫ ¬\underline{f}∨¬\underline{f} ⊢ \underline{f} ∨ ¬\underline{f}; ∀\underline{f}: ¬\underline{f} ∨ ¬\underline{f} ⊢ repeat ⊳ ¬\underline{f} ∨ ¬\underline{f} ≫ ¬\underline{f} ∨ ¬\underline{f}; pcdeduction ⊳ ∀\underline{f}: ¬\underline{f} ∨ ¬\underline{f} ⊢ ¬\underline{f} ∨ ¬\underline{f} ≫ ¬\underline{f} ∨ ¬\underline{f} ⊢ ¬\underline{f} ∨ ¬\underline{f}; notintro ⊳ ¬\underline{f} ∨ ¬\underline{f} ⊢ \underline{f} ∨ ¬\underline{f} ⊳ ¬\underline{f} ∨ ¬\underline{f} ⊢ ¬\underline{f} ∨ ¬\underline{f} ≫ ¬¬\underline{f} ∨ ¬\underline{f}; notnotelim ⊳ ¬¬\underline{f} ∨ ¬\underline{f} ≫ \underline{f} ∨ ¬\underline{f}⌉, p_{0}, c)]

[lem →^{stmt} pred calc ⊢ ∀\underline{f}: \underline{f} ∨ ¬\underline{f}]

[lem →^{pyk} “lem”]

forallintro

[forallintro →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ∀\underline{x}: ⌈\underline{x}⌉#^{0}⌈\underline{g} ∨ ¬\underline{g}⌉ ⊢⊢ \underline{f} ⊢ lem ≫ \underline{g} ∨ ¬\underline{g}; ∀\underline{g}: ∀\underline{f}: \underline{g} ∨ ¬\underline{g} ⊢ repeat ⊳ \underline{f} ≫ \underline{f}; pcdeduction ⊳ ∀\underline{g}: ∀\underline{f}: \underline{g} ∨ ¬\underline{g} ⊢ \underline{f} ≫ \underline{g} ∨ ¬\underline{g} ⇒ \underline{f}; pcia ⊳ ⊳ ⌈\underline{x}⌉#^{0}⌈\underline{g} ∨ ¬\underline{g}⌉ ⊳ \underline{g} ∨ ¬\underline{g} ⇒ \underline{f} ≫ \underline{g} ∨ ¬\underline{g} ⇒ ∀\underline{x}. (\underline{f}) ; pcmp ⊳ \underline{g} ∨ ¬\underline{g} ⊳ \underline{g} ∨ ¬\underline{g} ⇒ ∀\underline{x}. (\underline{f}) ≫ ∀\underline{x}. (\underline{f})⌉, p_{0}, c)]

[forallintro →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: ∀\underline{x}: ⌈\underline{x}⌉#^{0}⌈\underline{g} ∨ ¬\underline{g}⌉ ⊢⊢ \underline{f} ⊢ ∀\underline{x}. (\underline{f})]

[forallintro →^{pyk} “forallintro”]

forallelim

[forallelim →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{x}: ∀\underline{r}: ∀\underline{g}: ∀\underline{f}: ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊢⊢ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ⊢⊢ pc11 ⊳ ⊳ ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊳ ⊳ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊳ ⊳ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ≫ ∀\underline{x}. (\underline{f}) ⇒ \underline{g}; ∀\underline{x}: ∀\underline{g}: ∀\underline{f}: ∀\underline{x}. (\underline{f}) ⊢ pcmp ⊳ ∀\underline{x}. (\underline{f}) ⊳ ∀\underline{x}. (\underline{f}) ⇒ \underline{g} ≫ \underline{g}; pcdeduction ⊳ ∀\underline{x}: ∀\underline{g}: ∀\underline{f}: ∀\underline{x}. (\underline{f}) ⊢ \underline{g} ≫ ∀\underline{x}. (\underline{f}) ⊢ \underline{g}⌉, p_{0}, c)] [forallelim →^{stmt} pred calc ⊢ ∀\underline{x}: ∀\underline{r}: ∀\underline{g}: ∀\underline{f}: ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊢⊢ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ⊢⊢ ∀\underline{x}. (\underline{f}) ⊢ \underline{g}]

[forallelim →^{pyk} “forallelim”]

existsintro

[existsintro →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{x}: ∀\underline{r}: ∀\underline{g}: ∀\underline{f}: ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊢⊢ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ⊢⊢ pc12 ⊳ ⊳ ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊳ ⊳ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊳ ⊳ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ≫ \underline{g} ⇒ ∃\underline{x}. (\underline{f}) ; ∀\underline{x}: ∀\underline{g}: ∀\underline{f}: \underline{g} ⊢ pcmp ⊳ \underline{g} ⊳ \underline{g} ⇒ ∃\underline{x}. (\underline{f}) ≫ ∃\underline{x}. (\underline{f}) ; pcdeduction ⊳ ∀\underline{x}: ∀\underline{g}: ∀\underline{f}: \underline{g} ⊢ ∃\underline{x}. (\underline{f}) ≫ \underline{g} ⊢ ∃\underline{x}. (\underline{f})⌉, p_{0}, c)]

[existsintro →^{stmt} pred calc ⊢ ∀\underline{x}: ∀\underline{r}: ∀\underline{g}: ∀\underline{f}: ⌈\underline{x}⌉#^{0}⌈\underline{r}⌉ ⊢⊢ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ⟨⌈\underline{g}⌉≡^{0}⌈\underline{f}⌉|⌈\underline{x}⌉:=⌈\underline{r}⌉⟩ ⊢⊢ \underline{g} ⊢ ∃\underline{x}. (\underline{f})]

[existsintro →^{pyk} “existsintro”]

existselim

[existselim →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{x}: ∀\underline{f}: ∀\underline{g}: ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ∃\underline{x}. (\underline{f}) ⊢ \underline{f} ⊢ \underline{g} ⊢ pcded ⊳ \underline{f} ⊢ \underline{g} ≫ \underline{f} ⇒ \underline{g}; pcie ⊳ ⊳ ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊳ \underline{f} ⇒ \underline{g} ≫ ∃\underline{x}. (\underline{f}) ⇒ \underline{g}; pcmp ⊳ ∃\underline{x}. (\underline{f}) ⊳ ∃\underline{x}. (\underline{f}) ⇒ \underline{g} ≫ \underline{g}⌉, p_{0}, c)]

[existselim →^{stmt} pred calc ⊢ ∀\underline{x}: ∀\underline{f}: ∀\underline{g}: ⌈\underline{x}⌉#^{0}⌈\underline{g}⌉ ⊢⊢ ∃\underline{x}. (\underline{f}) ⊢ \underline{f} ⊢ \underline{g} ⊢ \underline{g}]

[existselim →^{pyk} “existselim”]

bottomelim

[bottomelim →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ ¬\underline{f} ⊢ ∀\underline{f}: ∀\underline{g}: ¬\underline{g} ⊢ andelim1 ⊳ \underline{f} ∧ ¬\underline{f} ≫ \underline{f}; pcdeduction ⊳ ∀\underline{f}: ∀\underline{g}: ¬\underline{g} ⊢ \underline{f} ≫ ¬\underline{g} ⊢ \underline{f}; ∀\underline{f}: ∀\underline{g}: ¬\underline{g} ⊢ andelim2 ⊳ \underline{f} ∧ ¬\underline{f} ≫ ¬\underline{f}; pcdeduction ⊳ ∀\underline{f}: ∀\underline{g}: ¬\underline{g} ⊢ ¬\underline{f} ≫ ¬\underline{g} ⊢ ¬\underline{f}; notintro ⊳ ¬\underline{g} ⊢ \underline{f} ⊳ ¬\underline{g} ⊢ ¬\underline{f} ≫ ¬¬\underline{g}; notnotelim ⊳ ¬¬\underline{g} ≫ \underline{g}⌉, p_{0}, c)]

[bottomelim →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ∧ ¬\underline{f} ⊢ \underline{g}]

[bottomelim →^{pyk} “bottomelim”]

lemnotintro

[lemnotintro →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ∧ ¬\underline{g} ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ pcmp⊳\underline{f} ⊳\underline{f} ⇒ \underline{g} ∧¬\underline{g} ≫ \underline{g} ∧¬\underline{g}; andelim1⊳\underline{g} ∧¬\underline{g} ≫ \underline{g}; pcdeduction⊳∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ \underline{g} ≫ \underline{f} ⊢ \underline{g}; ∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ pcmp ⊳ \underline{f} ⊳ \underline{f} ⇒ \underline{g} ∧ ¬\underline{g} ≫ \underline{g} ∧ ¬\underline{g}; andelim2 ⊳ \underline{g} ∧ ¬\underline{g} ≫ ¬\underline{g}; pcdeduction⊳∀\underline{f}: ∀\underline{g}: \underline{f} ⊢ ¬\underline{g} ≫ \underline{f} ⊢ ¬\underline{g}; notintro⊳\underline{f} ⊢ \underline{g}⊳\underline{f} ⊢ ¬\underline{g} ≫ ¬\underline{f}⌉, p_{0}, c)]

[lemnotintro →^{stmt} pred calc ⊢ ∀\underline{f}: ∀\underline{g}: \underline{f} ⇒ \underline{g} ∧ ¬\underline{g} ⊢ ¬\underline{f}]

[lemnotintro →^{pyk} “lemnotintro”]

nontriv0

[nontriv0 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{p}: ∀\underline{q}: \underline{p} ⇒ \underline{q} ⇒ \underline{q} ⊢ \underline{q} ⇒ \underline{p} ⊢ \underline{p} ⇒ \underline{q} ⊢ pcmp ⊳ \underline{p} ⇒ \underline{q} ⊳ \underline{p} ⇒ \underline{q} ⇒ \underline{q} ≫ \underline{q}; pcmp ⊳ \underline{q} ⊳ \underline{q} ⇒ \underline{p} ≫ \underline{p}⌉, p_{0}, c)]

[nontriv0 →^{stmt} pred calc ⊢ ∀\underline{p}: ∀\underline{q}: \underline{p} ⇒ \underline{q} ⇒ \underline{q} ⊢ \underline{q} ⇒ \underline{p} ⊢ \underline{p} ⇒ \underline{q} ⊢ \underline{p}]

[nontriv0 →^{pyk} “nontriv0”]

nontriv1

[nontriv1 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{p}: ∀\underline{q}: \underline{p} ⊢ ¬\underline{p} ⊢ andintro ⊳ \underline{p} ⊳ ¬\underline{p} ≫ \underline{p} ∧ ¬\underline{p}; bottomelim ⊳ \underline{p} ∧ ¬\underline{p} ≫ \underline{q}⌉, p_{0}, c)]

[nontriv1 →^{stmt} pred calc ⊢ ∀\underline{p}: ∀\underline{q}: \underline{p} ⊢ ¬\underline{p} ⊢ \underline{q}]

[nontriv1 →^{pyk} “nontriv1”]

nontriv2

[nontriv2 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{p}: ∀\underline{q}: ¬\underline{p} ⇒ \underline{q} ⊢ ¬\underline{p} ⊢ ∀\underline{p}: ∀\underline{q}: \underline{p} ⊢ nontriv1 ⊳ \underline{p} ⊳ ¬\underline{p} ≫ \underline{q}; pcdeduction ⊳ ∀\underline{p}: ∀\underline{q}: \underline{p} ⊢ \underline{q} ≫ \underline{p} ⇒ \underline{q}; andintro ⊳ \underline{p} ⇒ \underline{q} ⊳ ¬\underline{p} ⇒ \underline{q} ≫ \underline{p} ⇒ \underline{q} ∧ ¬\underline{p} ⇒ \underline{q}⌉, p_{0}, c)]

[nontriv2 →^{stmt} pred calc ⊢ ∀\underline{p}: ∀\underline{q}: ¬\underline{p} ⇒ \underline{q} ⊢ ¬\underline{p} ⊢ \underline{p} ⇒ \underline{q} ∧ ¬\underline{p} ⇒ \underline{q}]

[nontriv2 →^{pyk} “nontriv2”]

nontriv3

[nontriv3 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{p}: ∀\underline{q}: ¬\underline{p} ⇒ \underline{q} ⊢ ∀\underline{p}: ∀\underline{q}: ¬\underline{p} ⊢ nontriv2 ⊳ ¬\underline{p} ⇒ \underline{q} ⊳ ¬\underline{p} ≫ \underline{p} ⇒ \underline{q} ∧ ¬\underline{p} ⇒ \underline{q}; pcdeduction ⊳ ∀\underline{p}: ∀\underline{q}: ¬\underline{p} ⊢ \underline{p} ⇒ \underline{q} ∧ ¬\underline{p} ⇒ \underline{q} ≫ ¬\underline{p} ⇒ \underline{p} ⇒ \underline{q} ∧ ¬\underline{p} ⇒ \underline{q}; lemnotintro ⊳ ¬\underline{p} ⇒ \underline{p} ⇒ \underline{q} ∧ ¬\underline{p} ⇒ \underline{q} ≫ ¬¬\underline{p}; notnotelim ⊳ ¬¬\underline{p} ≫ \underline{p}⌉, p_{0}, c)]

[nontriv3 →^{stmt} pred calc ⊢ ∀\underline{p}: ∀\underline{q}: ¬\underline{p} ⇒ \underline{q} ⊢ \underline{p}] [nontriv3 →^{pyk} “nontriv3”]

nontriv4

[nontriv4 →^{proof} λc.λx.P(⌈pred calc ⊢ ∀\underline{p}: ∀\underline{q}: \underline{p} ⇒ \underline{q} ⇒ \underline{q} ⊢ \underline{q} ⇒ \underline{p} ⊢ ∀\underline{p}: ∀\underline{q}: \underline{p} ⇒ \underline{q} ⊢ nontriv0 ⊳ \underline{p} ⇒ \underline{q} ⇒ \underline{q} ⊳ \underline{q} ⇒ \underline{p} ⊳ \underline{p} ⇒ \underline{q} ≫ \underline{p}; pcdeduction ⊳ ∀\underline{p}: ∀\underline{q}: \underline{p} ⇒ \underline{q} ⊢ \underline{p} ≫ \underline{q} ⇒ \underline{q} ⊢ \underline{p}; ∀\underline{p}: ∀\underline{q}: ¬\underline{p} ⇒ \underline{q} ⊢ nontriv3 ⊳ ¬\underline{p} ⇒ \underline{q} ≫ \underline{p}; pcdeduction ⊳ ∀\underline{p}: ∀\underline{q}: ¬\underline{p} ⇒ \underline{q} ⊢ \underline{p} ≫ ¬\underline{p} ⇒ \underline{q} ⊢ \underline{p}; orelim ⊳ \underline{q} ⇒ \underline{q} ⊢ \underline{p} ⊳ ¬\underline{p} ⇒ \underline{q} ⊢ \underline{p} ≫ \underline{p}⌉, p_{0}, c)] [nontriv4 →^{stmt} pred calc ⊢ ∀\underline{p}: ∀\underline{q}: \underline{p} ⇒ \underline{q} ⇒ \underline{q} ⊢ \underline{q} ⇒ \underline{p} ⊢ \underline{p}] [nontriv4 →^{pyk} “nontriv4”]

nontriv5

[nontriv5 →^{pyk} “nontriv5”]

nontriv6

[nontriv6 →^{pyk} “nontriv6”]

∗ ≡ ∗

[y ≡ b →^{tex} “#1. \equiv #2.”] [∗ ≡ ∗ →^{pyk} “" setequiv "”]

∗ = ∗

[y = b →^{tex} “#1. = #2.”]

[∗ = ∗ →^{pyk} “" setequals "”]

¬∗

[¬x →^{tex} “\neg #1.”]

[¬∗ →^{pyk} “lnot "”]

∗ ∧ ∗

[x ∧ y →^{tex} “#1. \wedge #2.”]

[∗ ∧ ∗ →^{pyk} “" land "”]

∗ ∨ ∗

[x ∨ y →^{tex} “#1. \vee #2.”]

[∗ ∨ ∗ →^{pyk} “" lor "”]

∀ ∗ . (∗)

[∀y. (b) →^{tex} “\forall #1. . \left(#2.\right)”] [∀ ∗ . (∗) →^{pyk} “forall " dot " end forall”]

∃ ∗ . (∗)

[∃y. (b) →^{tex} “\exists #1. . \left(#2.\right)”] [∃ ∗ . (∗) →^{pyk} “exists " dot " end exists”]

∗ ∈ ∗

[y ∈ b →^{tex} “#1. \in #2.”]

[∗ ∈ ∗ →^{pyk} “" setin "”] The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-07-12.UTC:19:00:11.024866 = MJD-53928.TAI:19:00:44.024866 = LGT-4659447644024866e-6