---

Step * 1 of Lemma FOL-proveable-evidence

.....assertion..... 
1. [s] : mFOL-sequent()
2. pf : proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
3. [%2] : correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;pf)
⊢ ∀s:mFOL-sequent(). (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;pf) ⇒ FOL-sequent-evidence{i:l}(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 ⌜FOLeffect(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 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 `FOLRule-induction` [⌜parm{i'}⌝]⋅
   THEN (BHyp -1 THENA Auto)
   THEN Thin (-1)
   THEN Auto
   THEN RepUR ``FOLeffect mFO-dest-connective mFO-dest-quantifier`` (-1)
   THEN MoveToConcl (-1)
   THEN Progress (Repeat (AutoSplit))⋅
   THEN Auto
   THEN Reduce (-1)
   THEN Try (((Assert FOL-sequent-evidence{i:l}(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 FOL-sequent-evidence{i:l}(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
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. ↑mFOconnect?(concl)
8. mFOconnect-knd(concl) = "and" ∈ Atom
9. [<hyps, mFOconnect-left(concl)>; <hyps, mFOconnect-right(concl)>] = subgoals ∈ (mFOL-sequent() List)
10. FOL-sequent-evidence{i:l}(<hyps, mFOconnect-left(concl)>)
11. FOL-sequent-evidence{i:l}(<hyps, mFOconnect-right(concl)>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

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

3
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. var : ℤ
8. ¬(var ∈ mFOL-sequent-freevars(<hyps, concl>))
9. ↑mFOquant?(concl)
10. mFOquant-isall(concl) = tt
11. [<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>] = subgoals ∈ (mFOL-sequent() List)
12. FOL-sequent-evidence{i:l}(<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

4
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. var : ℤ
8. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
9. ↑mFOquant?(concl)
10. mFOquant-isall(concl) = ff
11. [<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>] = subgoals ∈ (mFOL-sequent() List)
12. FOL-sequent-evidence{i:l}(<hyps, mFOquant-body(concl)[var/mFOquant-var(concl)]>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

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

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

7
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. (concl ∈ hyps)
8. [] = subgoals ∈ (mFOL-sequent() List)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

8
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. hypnum : ℕ
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. FOL-sequent-evidence{i:l}(<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

9
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. hypnum : ℕ
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. FOL-sequent-evidence{i:l}(<[mFOconnect-left(hyps[hypnum]) / hyps], concl>)
13. FOL-sequent-evidence{i:l}(<[mFOconnect-right(hyps[hypnum]) / hyps], concl>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

10
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. hypnum : ℕ
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. FOL-sequent-evidence{i:l}(<hyps, mFOconnect-left(hyps[hypnum])>)
13. FOL-sequent-evidence{i:l}(<[mFOconnect-right(hyps[hypnum]) / hyps], concl>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

11
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. hypnum : ℕ
8. var : ℤ
9. hypnum < ||hyps||
10. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
11. ↑mFOquant?(hyps[hypnum])
12. mFOquant-isall(hyps[hypnum]) = tt
13. [<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>] = subgoals ∈ (mFOL-sequent() List)
14. FOL-sequent-evidence{i:l}(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

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

13
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. hypnum : ℕ
8. hypnum < ||hyps||
9. let n,vars = dest-atomic(hyps[hypnum]) in
   if n =a "false" ∧b null(vars) then inl [] else inr ⋅  fi 
= (inl subgoals)
∈ (mFOL-sequent() List?)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

---

Latex:

---

Latex:
.....assertion..... 
1.  [s]  :  mFOL-sequent()
2.  pf  :  proof-tree(mFOL-sequent();FOLRule();\mlambda{}sr.FOLeffect(sr))
3.  [\%2]  :  correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(sr);s;pf)
\mvdash{}  \mforall{}s:mFOL-sequent()
        (correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(sr);s;pf)  {}\mRightarrow{}  FOL-sequent-evidence\{i:l\}(s))


By

---

Latex:
(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{}FOLeffect(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  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  `FOLRule-induction`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{}
  THEN  (BHyp  -1  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto
  THEN  RepUR  ``FOLeffect  mFO-dest-connective  mFO-dest-quantifier``  (-1)
  THEN  MoveToConcl  (-1)
  THEN  Progress  (Repeat  (AutoSplit))\mcdot{}
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  Try  (((Assert  FOL-sequent-evidence\{i:l\}(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  FOL-sequent-evidence\{i:l\}(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{}))

---

Home Index