---

Step * of Lemma proof-tree-ext

∀[Sequent,Rule:Type]. ∀[effect:(Sequent × Rule) ⟶ (Sequent List?)].
  proof-tree(Sequent;Rule;effect) ≡ sr:Sequent × Rule × (case effect sr
                                                         of inl(subgoals) =>
                                                         ℕ||subgoals||
                                                         | inr(x) =>
                                                         Void ⟶ proof-tree(Sequent;Rule;effect))
BY
{ TACTIC:(Auto
          THEN (InstLemma `W-ext` [⌜Sequent × Rule⌝;⌜λ2sr.case effect sr
                                                      of inl(subgoals) =>
                                                      ℕ||subgoals||
                                                      | inr(x) =>
                                                      Void⌝]⋅
                THENA Auto
                )
          THEN Fold `proof-tree` (-1)
          THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[Sequent,Rule:Type].  \mforall{}[effect:(Sequent  \mtimes{}  Rule)  {}\mrightarrow{}  (Sequent  List?)].
    proof-tree(Sequent;Rule;effect)  \mequiv{}  sr:Sequent  \mtimes{}  Rule  \mtimes{}  (case  effect  sr
                                                                                                                  of  inl(subgoals)  =>
                                                                                                                  \mBbbN{}||subgoals||
                                                                                                                  |  inr(x)  =>
                                                                                                                  Void  {}\mrightarrow{}  proof-tree(Sequent;Rule;effect))


By

---

Latex:
TACTIC:(Auto
                THEN  (InstLemma  `W-ext`  [\mkleeneopen{}Sequent  \mtimes{}  Rule\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}sr.case  effect  sr
                                                                                                        of  inl(subgoals)  =>
                                                                                                        \mBbbN{}||subgoals||
                                                                                                        |  inr(x)  =>
                                                                                                        Void\mkleeneclose{}]\mcdot{}
                            THENA  Auto
                            )
                THEN  Fold  `proof-tree`  (-1)
                THEN  Trivial)

---

Home Index