---

Step * 1 2 of Lemma correct_proof_wf


1. Sequent : Type
2. Rule : Type
3. effect : (Sequent × Rule) ⟶ (Sequent List?)
4. a : Sequent × Rule
5. f : case effect a of inl(subgoals) => ℕ||subgoals|| | inr(x) => Void ⟶ W(Sequent × Rule;a.case effect a
                                                                            of inl(subgoals) =>
                                                                            ℕ||subgoals||
                                                                            | inr(x) =>
                                                                            Void)
6. ∀b:case effect a of inl(subgoals) => ℕ||subgoals|| | inr(x) => Void. ∀s:Sequent.
     (correct_proof(Sequent;effect;s;f b) ∈ ℙ)
7. s : Sequent@i
8. x : Sequent List@i
9. (effect a) = (inl x) ∈ (Sequent List?)
10. i : ℕ||x||@i
11. i = i ∈ ℕ||x||
⊢ ℕ||x|| ⊆r case effect a of inl(subgoals) => ℕ||subgoals|| | inr(x) => Void
BY
{ TACTIC:(HypSubst' (-3) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  Sequent  :  Type
2.  Rule  :  Type
3.  effect  :  (Sequent  \mtimes{}  Rule)  {}\mrightarrow{}  (Sequent  List?)
4.  a  :  Sequent  \mtimes{}  Rule
5.  f  :  case  effect  a  of  inl(subgoals)  =>  \mBbbN{}||subgoals||  |  inr(x)  =>  Void
{}\mrightarrow{}  W(Sequent  \mtimes{}  Rule;a.case  effect  a  of  inl(subgoals)  =>  \mBbbN{}||subgoals||  |  inr(x)  =>  Void)
6.  \mforall{}b:case  effect  a  of  inl(subgoals)  =>  \mBbbN{}||subgoals||  |  inr(x)  =>  Void.  \mforall{}s:Sequent.
          (correct\_proof(Sequent;effect;s;f  b)  \mmember{}  \mBbbP{})
7.  s  :  Sequent@i
8.  x  :  Sequent  List@i
9.  (effect  a)  =  (inl  x)
10.  i  :  \mBbbN{}||x||@i
11.  i  =  i
\mvdash{}  \mBbbN{}||x||  \msubseteq{}r  case  effect  a  of  inl(subgoals)  =>  \mBbbN{}||subgoals||  |  inr(x)  =>  Void


By

---

Latex:
TACTIC:(HypSubst'  (-3)  0  THEN  Reduce  0  THEN  Auto)

---

Home Index