---

Step * of Lemma proof_tree_ind_wf

No Annotations
∀[Sequent,Rule:Type]. ∀[effect:(Sequent × Rule) ⟶ (Sequent List?)]. ∀[Q:proof-tree(Sequent;Rule;effect) ⟶ ℙ].
∀[abort:∀s:Sequent. ∀r:Rule.  Q[proof-abort(s;r)] supposing ↑isr(effect <s, r>)].
∀[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>)]. ∀[pf:proof-tree(Sequent;Rule;effect)].
  (proof_tree_ind(effect;abort;progress;pf) ∈ Q[pf])
BY
{ (Auto
   THEN (Assert ⌜TERMOF{proof-tree-induction-ext:o, \\v:l, i:l} ∈ ∀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>)|| \000C∈ ℤ 
                                                                            supposing ↑isl(effect <s, r>))
                                                                      ⇒ (∀pf:proof-tree(Sequent;Rule;effect). Q[pf]))⌝⋅
         THENA Auto
         )
   THEN (Assert ⌜TERMOF{proof-tree-induction-ext:o, \\v:l, i:l} 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])⌝⋅
         THENA Auto
         )
   THEN Thin (-2)
   THEN (Assert TERMOF{proof-tree-induction-ext:o, \\v:l, i:l} effect abort progress
                ∈ ∀pf:proof-tree(Sequent;Rule;effect). Q[pf] BY
               Auto)
   THEN Thin (-2)⋅) }

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]
⊢ proof_tree_ind(effect;abort;progress;pf) ∈ Q[pf]

---

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{}[abort:\mforall{}s:Sequent.  \mforall{}r:Rule.
                                                                                                          Q[proof-abort(s;r)] 
                                                                                                          supposing  \muparrow{}isr(effect  <s,  r>)].
\mforall{}[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>)|| 
                          supposing  \muparrow{}isl(effect  <s,  r>)].  \mforall{}[pf:proof-tree(Sequent;Rule;effect)].
    (proof\_tree\_ind(effect;abort;progress;pf)  \mmember{}  Q[pf])


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}TERMOF\{proof-tree-induction-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}
                              \mmember{}  \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]))\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  (Assert  \mkleeneopen{}TERMOF\{proof-tree-induction-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  effect  \mmember{}  (\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])\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  Thin  (-2)
  THEN  (Assert  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]  BY
                          Auto)
  THEN  Thin  (-2)\mcdot{})

---

Home Index