---

Step * of Lemma sq_stable__correct_proof

∀[Sequent,Rule:Type].
  ∀effect:(Sequent × Rule) ⟶ (Sequent List?)
    ∀[s:Sequent]. ∀pf:proof-tree(Sequent;Rule;effect). SqStable(correct_proof(Sequent;effect;s;pf))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN UseWitness ⌜fix((λcorrect_proof,pf. let sr,f = pf 
                                            in <Ax
                                               , case effect sr
                                                  of inl(subgoals) =>
                                                  λi.(correct_proof (f i))
                                                  | inr(x) =>
                                                  ⋅
                                               >)) 
                    pf⌝⋅
   THEN MoveToConcl (-3)
   THEN Unfold `proof-tree` -1
   THEN WElim (-1)
   THEN Unfold `it` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN RepUR ``Wsup`` 0
   THEN RecUnfold `correct_proof` 0
   THEN Reduce 0
   THEN (GenConclTerm ⌜effect a⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN Try ((DoSubsume THEN Auto THEN HypSubst' (-5) 0 THEN Auto))
   THEN InstHyp [⌜i⌝;⌜x[i]⌝] (-7)⋅
   THEN Auto
   THEN Try ((DoSubsume THEN Auto THEN HypSubst' (-6) 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[Sequent,Rule:Type].
    \mforall{}effect:(Sequent  \mtimes{}  Rule)  {}\mrightarrow{}  (Sequent  List?)
        \mforall{}[s:Sequent].  \mforall{}pf:proof-tree(Sequent;Rule;effect).  SqStable(correct\_proof(Sequent;effect;s;pf))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  UseWitness  \mkleeneopen{}fix((\mlambda{}correct$_{proof}$,pf.  let  sr,f  =  pf 
                                                                                  in  <Ax
                                                                                        ,  case  effect  sr
                                                                                              of  inl(subgoals)  =>
                                                                                              \mlambda{}i.(correct$_{proof}$  (f  i))
                                                                                              |  inr(x)  =>
                                                                                              \mcdot{}
                                                                                        >)) 
                                    pf\mkleeneclose{}\mcdot{}
  THEN  MoveToConcl  (-3)
  THEN  Unfold  `proof-tree`  -1
  THEN  WElim  (-1)
  THEN  Unfold  `it`  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  RepUR  ``Wsup``  0
  THEN  RecUnfold  `correct\_proof`  0
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}effect  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto  THEN  HypSubst'  (-5)  0  THEN  Auto))
  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}x[i]\mkleeneclose{}]  (-7)\mcdot{}
  THEN  Auto
  THEN  Try  ((DoSubsume  THEN  Auto  THEN  HypSubst'  (-6)  0  THEN  Auto)))

---

Home Index