---

Step * of Lemma proof-tree-induction

No Annotations
∀[Sequent,Rule:Type].
  ∀effect:(Sequent × Rule) ⟶ (Sequent List?)
    ∀[Q:proof-tree(Sequent;Rule;effect) ⟶ ℙ]
      ((∀s:Sequent. ∀r:Rule.  Q[proof-abort(s;r)] supposing ↑isr(effect <s, r>))
      ⇒ (∀s:Sequent. ∀r:Rule.
            ∀L:proof-tree(Sequent;Rule;effect) List
              (∀pf∈L.Q[pf]) ⇒ Q[make-proof-tree(s;r;L)] supposing ||L|| = ||outl(effect <s, r>)|| ∈ ℤ 
            supposing ↑isl(effect <s, r>))
      ⇒ (∀pf:proof-tree(Sequent;Rule;effect). Q[pf]))
BY
{ (Auto
   THEN All
   (Unfold `proof-tree`)⋅
   THEN InstLemma `W-induction` [⌜Sequent × Rule⌝;⌜λ2sr.case effect sr
                                                    of inl(subgoals) =>
                                                    ℕ||subgoals||
                                                    | inr(x) =>
                                                    Void⌝;⌜Q⌝;⌜pf⌝]⋅
   THEN Auto
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenConclTerm ⌜effect a⌝⋅ THENA Auto)
   THEN D -1
   THEN Reduce 0
   THEN All (Fold `proof-tree`)
   THEN D -3
   THEN RenameVar `s' (-4)
   THEN RenameVar `r' (-3)
   THEN D -2
   THEN Reduce 0
   THEN ∀h:hyp. (InstHyp [⌜s⌝;⌜r⌝] h⋅ THENA Complete ((Auto THEN HypSubst' (-1) 0 THEN Auto))) 
   THEN Auto) }

1
1. [Sequent] : Type
2. [Rule] : Type
3. effect : (Sequent × Rule) ⟶ (Sequent List?)
4. [Q] : proof-tree(Sequent;Rule;effect) ⟶ ℙ
5. ∀s:Sequent. ∀r:Rule.  Q[proof-abort(s;r)] supposing ↑isr(effect <s, r>)
6. ∀s:Sequent. ∀r:Rule.
     ∀L:proof-tree(Sequent;Rule;effect) List
       (∀pf∈L.Q[pf]) ⇒ Q[make-proof-tree(s;r;L)] supposing ||L|| = ||outl(effect <s, r>)|| ∈ ℤ 
     supposing ↑isl(effect <s, r>)
7. pf : proof-tree(Sequent;Rule;effect)
8. s : Sequent
9. r : Rule
10. x : Sequent List
11. (effect <s, r>) = (inl x) ∈ (Sequent List?)
12. ∀L:proof-tree(Sequent;Rule;effect) List
      (∀pf∈L.Q[pf]) ⇒ Q[make-proof-tree(s;r;L)] supposing ||L|| = ||outl(effect <s, r>)|| ∈ ℤ
13. f : ℕ||x|| ⟶ proof-tree(Sequent;Rule;effect)
14. ∀b:ℕ||x||. Q[f b]
⊢ Q[Wsup(<s, r>;f)]

2
1. [Sequent] : Type
2. [Rule] : Type
3. effect : (Sequent × Rule) ⟶ (Sequent List?)
4. [Q] : proof-tree(Sequent;Rule;effect) ⟶ ℙ
5. ∀s:Sequent. ∀r:Rule.  Q[proof-abort(s;r)] supposing ↑isr(effect <s, r>)
6. ∀s:Sequent. ∀r:Rule.
     ∀L:proof-tree(Sequent;Rule;effect) List
       (∀pf∈L.Q[pf]) ⇒ Q[make-proof-tree(s;r;L)] supposing ||L|| = ||outl(effect <s, r>)|| ∈ ℤ 
     supposing ↑isl(effect <s, r>)
7. pf : proof-tree(Sequent;Rule;effect)
8. s : Sequent
9. r : Rule
10. y : Unit
11. (effect <s, r>) = (inr y ) ∈ (Sequent List?)
12. Q[proof-abort(s;r)]
13. f : Void ⟶ proof-tree(Sequent;Rule;effect)
14. ∀b:Void. Q[f b]
⊢ Q[Wsup(<s, r>;f)]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Sequent,Rule:Type].
    \mforall{}effect:(Sequent  \mtimes{}  Rule)  {}\mrightarrow{}  (Sequent  List?)
        \mforall{}[Q:proof-tree(Sequent;Rule;effect)  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}s:Sequent.  \mforall{}r:Rule.    Q[proof-abort(s;r)]  supposing  \muparrow{}isr(effect  <s,  r>))
            {}\mRightarrow{}  (\mforall{}s:Sequent.  \mforall{}r:Rule.
                        \mforall{}L:proof-tree(Sequent;Rule;effect)  List
                            (\mforall{}pf\mmember{}L.Q[pf])  {}\mRightarrow{}  Q[make-proof-tree(s;r;L)]  supposing  ||L||  =  ||outl(effect  <s,  r>)|| 
                        supposing  \muparrow{}isl(effect  <s,  r>))
            {}\mRightarrow{}  (\mforall{}pf:proof-tree(Sequent;Rule;effect).  Q[pf]))


By

---

Latex:
(Auto
  THEN  All
  (Unfold  `proof-tree`)\mcdot{}
  THEN  InstLemma  `W-induction`  [\mkleeneopen{}Sequent  \mtimes{}  Rule\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}sr.case  effect  sr
                                                                                                    of  inl(subgoals)  =>
                                                                                                    \mBbbN{}||subgoals||
                                                                                                    |  inr(x)  =>
                                                                                                    Void\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}pf\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}effect  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  Reduce  0
  THEN  All  (Fold  `proof-tree`)
  THEN  D  -3
  THEN  RenameVar  `s'  (-4)
  THEN  RenameVar  `r'  (-3)
  THEN  D  -2
  THEN  Reduce  0
  THEN  \mforall{}h:hyp.  (InstHyp  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]  h\mcdot{}  THENA  Complete  ((Auto  THEN  HypSubst'  (-1)  0  THEN  Auto))) 
  THEN  Auto)

---

Home Index