---

Step * 1 of Lemma mFOL-proveable-evidence

.....assertion..... 
1. [s] : mFOL-sequent()
2. pf : proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i
3. \\%2 : correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf)@i
⊢ ∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;pf) ⇒ mFOL-sequent-evidence(s))
BY
{ (All Thin
   THEN MoveToConcl (-1)
   THEN Unfold `proof-tree` 0
   THEN UseWInductionLemma'
   THEN Fold `proof-tree` (-2)
   THEN RecUnfold `correct_proof` 0
   THEN RepUR ``Wsup`` 0
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN Reduce 0
   THEN (GenConclTerm ⌈mFOLeffect(a)⌉⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN At ⌈𝕌'⌉ (Auto)⋅
   THEN Try ((Unfold `proof-tree` 0 THEN Complete (Auto)))
   THEN D 1
   THEN Reduce (-2)
   THEN RevHypSubst (-2) 0
   THEN Auto
   THEN RepeatFor 2 (Thin (-2))
   THEN D 1
   THEN RenameVar `hyps' 1
   THEN RenameVar `concl' 2
   THEN RenameVar `rule' 3
   THEN RenameVar `subgoals' 4
   THEN RenameVar `subproofs' 6
   THEN MoveToConcl 3
   THEN InstLemma `mFOLRule-induction` [⌈parm{i'}⌉]⋅
   THEN (BHyp -1  THENA Auto)
   THEN Thin (-1)
   THEN Auto
   THEN RepUR ``mFOLeffect mFO-dest-connective mFO-dest-quantifier`` (-1)
   THEN (Try ((MoveToConcl (-1) THEN Progress (Repeat (AutoSplit))⋅ THEN Auto THEN Reduce (-1)))
         THEN Try (((Assert mFOL-sequent-evidence(subgoals[0]) BY
                           ((Assert 0 < ||subgoals|| BY
                                   (RevHypSubst' (-1) 0 THEN Reduce 0 THEN Auto))
                            THEN (InstHyp [⌈0⌉] 5⋅ THENA Auto)
                            THEN BHyp -1 
                            THEN Complete (Auto)))
                    THEN (StrongRevHypSubst (-2) (-1) THENA (Auto THEN HypSubst (-1) 0 THEN Reduce 0 THEN Auto))
                    THEN Reduce (-1)))
         THEN Try (((Assert mFOL-sequent-evidence(subgoals[1]) BY
                           ((Assert 1 < ||subgoals|| BY
                                   (RevHypSubst' (-2) 0 THEN Reduce 0 THEN All Thin THEN Complete (Auto)))
                            THEN (InstHyp [⌈1⌉] 5⋅ THENA Auto)
                            THEN BHyp -1 
                            THEN Complete (Auto)))
                    THEN (StrongRevHypSubst (-3) (-1) THENA (Auto THEN HypSubst (-1) 0 THEN Reduce 0 THEN Auto))
                    THEN Reduce (-1))⋅))⋅) }

1
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. ↑mFOconnect?(concl)
8. mFOconnect-knd(concl) = "and" ∈ Atom
9. [<hyps, mFOconnect-left(concl)>; <hyps, mFOconnect-right(concl)>] = subgoals ∈ (mFOL-sequent() List)
10. mFOL-sequent-evidence(<hyps, mFOconnect-left(concl)>)
11. mFOL-sequent-evidence(<hyps, mFOconnect-right(concl)>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

2
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. ↑mFOconnect?(concl)
8. mFOconnect-knd(concl) = "imp" ∈ Atom
9. [<[mFOconnect-left(concl) / hyps], mFOconnect-right(concl)>] = subgoals ∈ (mFOL-sequent() List)
10. mFOL-sequent-evidence(<[mFOconnect-left(concl) / hyps], mFOconnect-right(concl)>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

3
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. var : ℤ@i
8. ¬(var ∈ mFOL-freevars(concl))
9. (∀h∈hyps.¬(var ∈ mFOL-freevars(h)))
10. ↑mFOquant?(concl)
11. mFOquant-isall(concl) = tt
12. [<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>] = subgoals ∈ (mFOL-sequent() List)
13. mFOL-sequent-evidence(<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

4
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. var : ℤ@i
8. ↑mFOquant?(concl)
9. mFOquant-isall(concl) = ff
10. [<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>] = subgoals ∈ (mFOL-sequent() List)
11. mFOL-sequent-evidence(<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

5
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. left : 𝔹@i
8. ↑mFOconnect?(concl)
9. mFOconnect-knd(concl) = "or" ∈ Atom
10. ↑left
11. [<hyps, mFOconnect-left(concl)>] = subgoals ∈ (mFOL-sequent() List)
12. mFOL-sequent-evidence(<hyps, mFOconnect-left(concl)>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

6
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. left : 𝔹@i
8. ¬↑left
9. ↑mFOconnect?(concl)
10. mFOconnect-knd(concl) = "or" ∈ Atom
11. [<hyps, mFOconnect-right(concl)>] = subgoals ∈ (mFOL-sequent() List)
12. mFOL-sequent-evidence(<hyps, mFOconnect-right(concl)>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

7
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. (concl ∈ hyps)
8. [] = subgoals ∈ (mFOL-sequent() List)
⊢ mFOL-sequent-evidence(<hyps, concl>)

8
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. hypnum : ℕ@i
8. hypnum < ||hyps||
9. ↑mFOconnect?(hyps[hypnum])
10. mFOconnect-knd(hyps[hypnum]) = "and" ∈ Atom
11. [<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>] = subgoals ∈ (mFOL-sequent() Lis\000Ct)
12. mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

9
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. hypnum : ℕ@i
8. hypnum < ||hyps||
9. ↑mFOconnect?(hyps[hypnum])
10. mFOconnect-knd(hyps[hypnum]) = "or" ∈ Atom
11. [<[mFOconnect-left(hyps[hypnum]) / hyps], concl>; <[mFOconnect-right(hyps[hypnum]) / hyps], concl>] = subgoals ∈ (mF\000COL-sequent() List)
12. mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]) / hyps], concl>)
13. mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum]) / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

10
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. hypnum : ℕ@i
8. hypnum < ||hyps||
9. ↑mFOconnect?(hyps[hypnum])
10. mFOconnect-knd(hyps[hypnum]) = "imp" ∈ Atom
11. [<hyps, mFOconnect-left(hyps[hypnum])>; <[mFOconnect-right(hyps[hypnum]) / hyps], concl>] = subgoals ∈ (mFOL-sequent\000C() List)
12. mFOL-sequent-evidence(<hyps, mFOconnect-left(hyps[hypnum])>)
13. mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum]) / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

11
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. hypnum : ℕ@i
8. var : ℤ@i
9. hypnum < ||hyps||
10. ↑mFOquant?(hyps[hypnum])
11. mFOquant-isall(hyps[hypnum]) = tt
12. [<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>] = subgoals ∈ (mFOL-sequent() List)
13. mFOL-sequent-evidence(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

12
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. subproofs : ℕ||subgoals|| ─→ proof-tree(mFOL-sequent();mFOLRule();λsr.mFOLeffect(sr))@i'
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);s;subproofs b) ⇒ mFOL-sequent-evidence(s))@i'
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.mFOLeffect(sr);subgoals[i];subproofs i)@i'
7. hypnum : ℕ@i
8. var : ℤ@i
9. ¬(var ∈ mFOL-freevars(concl))
10. hypnum < ||hyps||
11. (∀h∈hyps.¬(var ∈ mFOL-freevars(h)))
12. ↑mFOquant?(hyps[hypnum])
13. mFOquant-isall(hyps[hypnum]) = ff
14. [<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>] = subgoals ∈ (mFOL-sequent() List)
15. mFOL-sequent-evidence(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)

---

Latex:


.....assertion..... 
1.  [s]  :  mFOL-sequent()
2.  pf  :  proof-tree(mFOL-sequent();mFOLRule();\mlambda{}sr.mFOLeffect(sr))@i
3.  \mbackslash{}\mbackslash{}\%2  :  correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)@i
\mvdash{}  \mforall{}s:mFOL-sequent()
        (correct\_proof(mFOL-sequent();\mlambda{}sr.mFOLeffect(sr);s;pf)  {}\mRightarrow{}  mFOL-sequent-evidence(s))


By

(All  Thin
  THEN  MoveToConcl  (-1)
  THEN  Unfold  `proof-tree`  0
  THEN  UseWInductionLemma'
  THEN  Fold  `proof-tree`  (-2)
  THEN  RecUnfold  `correct\_proof`  0
  THEN  RepUR  ``Wsup``  0
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}mFOLeffect(a)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (Auto)\mcdot{}
  THEN  Try  ((Unfold  `proof-tree`  0  THEN  Complete  (Auto)))
  THEN  D  1
  THEN  Reduce  (-2)
  THEN  RevHypSubst  (-2)  0
  THEN  Auto
  THEN  RepeatFor  2  (Thin  (-2))
  THEN  D  1
  THEN  RenameVar  `hyps'  1
  THEN  RenameVar  `concl'  2
  THEN  RenameVar  `rule'  3
  THEN  RenameVar  `subgoals'  4
  THEN  RenameVar  `subproofs'  6
  THEN  MoveToConcl  3
  THEN  InstLemma  `mFOLRule-induction`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}
  THEN  (BHyp  -1    THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto
  THEN  RepUR  ``mFOLeffect  mFO-dest-connective  mFO-dest-quantifier``  (-1)
  THEN  (Try  ((MoveToConcl  (-1)  THEN  Progress  (Repeat  (AutoSplit))\mcdot{}  THEN  Auto  THEN  Reduce  (-1)))
              THEN  Try  (((Assert  mFOL-sequent-evidence(subgoals[0])  BY
                                                  ((Assert  0  <  ||subgoals||  BY
                                                                  (RevHypSubst'  (-1)  0  THEN  Reduce  0  THEN  Auto))
                                                    THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
                                                    THEN  BHyp  -1 
                                                    THEN  Complete  (Auto)))
                                    THEN  (StrongRevHypSubst  (-2)  (-1)
                                                THENA  (Auto  THEN  HypSubst  (-1)  0  THEN  Reduce  0  THEN  Auto)
                                                )
                                    THEN  Reduce  (-1)))
              THEN  Try  (((Assert  mFOL-sequent-evidence(subgoals[1])  BY
                                                  ((Assert  1  <  ||subgoals||  BY
                                                                  (RevHypSubst'  (-2)  0
                                                                    THEN  Reduce  0
                                                                    THEN  All  Thin
                                                                    THEN  Complete  (Auto)))
                                                    THEN  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
                                                    THEN  BHyp  -1 
                                                    THEN  Complete  (Auto)))
                                    THEN  (StrongRevHypSubst  (-3)  (-1)
                                                THENA  (Auto  THEN  HypSubst  (-1)  0  THEN  Reduce  0  THEN  Auto)
                                                )
                                    THEN  Reduce  (-1))\mcdot{}))\mcdot{})

---

Home Index