---

Step * of Lemma proof-tree-induction-ext

∀[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
{ Extract of Obid: proof-tree-induction
  not unfolding  W_ind primrec mklist length
  finishing with xxx(Try (Fold `proof_tree_ind` 0) THEN Auto)xxx
  normalizes to:
  
  λeffect,abort,progress,pf. proof_tree_ind(effect;abort;progress;pf) }

---

Latex:

---

Latex:
\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:
Extract  of  Obid:  proof-tree-induction
not  unfolding    W\_ind  primrec  mklist  length
finishing  with  xxx(Try  (Fold  `proof\_tree\_ind`  0)  THEN  Auto)xxx
normalizes  to:

\mlambda{}effect,abort,progress,pf.  proof\_tree\_ind(effect;abort;progress;pf)

---

Home Index