---

Step * 1 of Lemma proof-tree-induction


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)]
BY
{ ((Subst' ||outl(effect <s, r>)|| ~ ||x|| -3 THENA Auto) THEN InstHyp [⌜mklist(||x||;f)⌝] (-3)⋅ THEN Auto) }

1
.....antecedent..... 
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|| = ||x|| ∈ ℤ
13. f : ℕ||x|| ⟶ proof-tree(Sequent;Rule;effect)
14. ∀b:ℕ||x||. Q[f b]
⊢ (∀pf∈mklist(||x||;f).Q[pf])

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. 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|| = ||x|| ∈ ℤ
13. f : ℕ||x|| ⟶ proof-tree(Sequent;Rule;effect)
14. ∀b:ℕ||x||. Q[f b]
15. Q[make-proof-tree(s;r;mklist(||x||;f))]
⊢ Q[Wsup(<s, r>;f)]

---

Latex:

---

Latex:

1.  [Sequent]  :  Type
2.  [Rule]  :  Type
3.  effect  :  (Sequent  \mtimes{}  Rule)  {}\mrightarrow{}  (Sequent  List?)
4.  [Q]  :  proof-tree(Sequent;Rule;effect)  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}s:Sequent.  \mforall{}r:Rule.    Q[proof-abort(s;r)]  supposing  \muparrow{}isr(effect  <s,  r>)
6.  \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>)
7.  pf  :  proof-tree(Sequent;Rule;effect)
8.  s  :  Sequent
9.  r  :  Rule
10.  x  :  Sequent  List
11.  (effect  <s,  r>)  =  (inl  x)
12.  \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>)||
13.  f  :  \mBbbN{}||x||  {}\mrightarrow{}  proof-tree(Sequent;Rule;effect)
14.  \mforall{}b:\mBbbN{}||x||.  Q[f  b]
\mvdash{}  Q[Wsup(<s,  r>f)]


By

---

Latex:
((Subst'  ||outl(effect  <s,  r>)||  \msim{}  ||x||  -3  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}mklist(||x||;f)\mkleeneclose{}]  (-3)\mcdot{}  THEN  \000CAuto)

---

Home Index