---

Step * 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]
⊢ proof_tree_ind(effect;abort;progress;pf) ∈ Q[pf]
BY
{ TACTIC:(Unfold `all` -1
          THEN (Assert TERMOF{proof-tree-induction-ext:o, \\v:l, i:l} effect abort progress pf ∈ Q[pf] BY
                      Auto)
          THEN NthHypSq (-1)
          THEN EqCD
          THEN Auto) }

1
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

---

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{}  \mforall{}pf:proof-tree(Sequent;Rule;effect).  Q[pf]
\mvdash{}  proof\_tree\_ind(effect;abort;progress;pf)  \mmember{}  Q[pf]


By

---

Latex:
TACTIC:(Unfold  `all`  -1
                THEN  (Assert  TERMOF\{proof-tree-induction-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  effect  abort  progress  pf
                                          \mmember{}  Q[pf]  BY
                                        Auto)
                THEN  NthHypSq  (-1)
                THEN  EqCD
                THEN  Auto)

---

Home Index