---

Step * 1 1 of Lemma proof_tree_ind_wf


1. Sequent : Type
2. Rule : Type
3. effect : (Sequent × Rule) ⟶ (Sequent List?)
4. Q : proof-tree(Sequent;Rule;effect) ⟶ ℙ
5. abort : ∀s:Sequent. ∀r:Rule.  Q[proof-abort(s;r)] supposing ↑isr(effect <s, r>)
6. progress : ∀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. TERMOF{proof-tree-induction-ext:o, \\v:l, i:l} effect abort progress ∈ pf:proof-tree(Sequent;Rule;effect) ⟶ Q[pf]
9. TERMOF{proof-tree-induction-ext:o, \\v:l, i:l} effect abort progress pf ∈ Q[pf]
⊢ proof_tree_ind(effect;abort;progress;pf) ~ TERMOF{proof-tree-induction-ext:o, \\v:l, i:l} effect abort progress pf
BY
{ (RW (AddrC [2] (SymbCompC [] 3)) 0 THEN Reduce 0 THEN Auto) }

---

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.  abort  :  \mforall{}s:Sequent.  \mforall{}r:Rule.    Q[proof-abort(s;r)]  supposing  \muparrow{}isr(effect  <s,  r>)
6.  progress  :  \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>)\000C|| 
                                supposing  \muparrow{}isl(effect  <s,  r>)
7.  pf  :  proof-tree(Sequent;Rule;effect)
8.  TERMOF\{proof-tree-induction-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  effect  abort  progress
      \mmember{}  pf:proof-tree(Sequent;Rule;effect)  {}\mrightarrow{}  Q[pf]
9.  TERMOF\{proof-tree-induction-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  effect  abort  progress  pf  \mmember{}  Q[pf]
\mvdash{}  proof\_tree\_ind(effect;abort;progress;pf)  \msim{}  TERMOF\{proof-tree-induction-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  effect 
                                                                                          abort 
                                                                                          progress 
                                                                                          pf


By

---

Latex:
(RW  (AddrC  [2]  (SymbCompC  []  3))  0  THEN  Reduce  0  THEN  Auto)

---

Home Index