---

Step * 1 2 1 1 1 12 of Lemma mFOL-proveable-evidence


1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. hypnum : ℕ
6. var : ℤ
7. ¬(var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. hypnum < ||hyps||
9. ↑mFOquant?(hyps[hypnum])
10. mFOquant-isall(hyps[hypnum]) = ff
11. [<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>] = subgoals ∈ (mFOL-sequent() List)
12. mFOL-sequent-evidence(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
BY
{ ((Thin (-2) THEN Thin 4)
   THEN RenameVar `z' 5
   THEN D 0
   THEN Auto
   THEN Unfold `mFOL-sequent-abstract` 0
   THEN RepUR ``FOSatWith`` 0
   THEN Fold `FOSatWith` 0
   THEN Auto
   THEN ((Assert hyps[hypnum] = ∃mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum])) ∈ mFOL() BY
                (RepeatFor 2 (MoveToConcl (-6))
                 THEN GenConclAtAddr [1;1;1]
                 THEN All Thin
                 THEN MoveToConcl (-1)
                 THEN BLemmaUp `mFOL-induction`
                 THEN Reduce 0
                 THEN Auto
                 THEN Try ((Fold `AbstractFOFormula` 0 THEN Auto))
                 THEN Unfold `mFOL-sequent` 0
                 THEN Auto))
         THEN MoveToConcl (-1)⋅
         THEN MoveToConcl 10
         THEN (GenConcl ⌜mFOquant-body(hyps[hypnum]) = B ∈ mFOL()⌝⋅ THENA Auto)
         THEN (GenConcl ⌜mFOquant-var(hyps[hypnum]) = y ∈ ℤ⌝⋅ THENA Auto)
         THEN Auto)⋅) }

1
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. z : ℤ
6. ¬(z ∈ mFOL-sequent-freevars(<hyps, concl>))
7. hypnum < ||hyps||
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = ff
10. [Dom] : Type
11. [S] : FOStruct(Dom)
12. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
13. tuple-type(mFOL-hyps-meaning(Dom;S;a;hyps))
14. B : mFOL()
15. mFOquant-body(hyps[hypnum]) = B ∈ mFOL()
16. y : ℤ
17. mFOquant-var(hyps[hypnum]) = y ∈ ℤ
18. mFOL-sequent-evidence(<[B[z/y] / hyps], concl>)
19. hyps[hypnum] = ∃y;B) ∈ mFOL()
⊢ Dom,S,a |= mFOL-abstract(concl)

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  subgoals  :  mFOL-sequent()  List
4.  \mforall{}i:\mBbbN{}||subgoals||.  mFOL-sequent-evidence(subgoals[i])
5.  hypnum  :  \mBbbN{}
6.  var  :  \mBbbZ{}
7.  \mneg{}(var  \mmember{}  mFOL-sequent-freevars(<hyps,  concl>))
8.  hypnum  <  ||hyps||
9.  \muparrow{}mFOquant?(hyps[hypnum])
10.  mFOquant-isall(hyps[hypnum])  =  ff
11.  [<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]  /  hyps],  concl>]  =  subgoals
12.  mFOL-sequent-evidence(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]  /  hyps]
                                                    ,  concl
                                                    >)
\mvdash{}  mFOL-sequent-evidence(<hyps,  concl>)


By

---

Latex:
((Thin  (-2)  THEN  Thin  4)
  THEN  RenameVar  `z'  5
  THEN  D  0
  THEN  Auto
  THEN  Unfold  `mFOL-sequent-abstract`  0
  THEN  RepUR  ``FOSatWith``  0
  THEN  Fold  `FOSatWith`  0
  THEN  Auto
  THEN  ((Assert  hyps[hypnum]  =  \mexists{}mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum]))  BY
                            (RepeatFor  2  (MoveToConcl  (-6))
                              THEN  GenConclAtAddr  [1;1;1]
                              THEN  All  Thin
                              THEN  MoveToConcl  (-1)
                              THEN  BLemmaUp  `mFOL-induction`
                              THEN  Reduce  0
                              THEN  Auto
                              THEN  Try  ((Fold  `AbstractFOFormula`  0  THEN  Auto))
                              THEN  Unfold  `mFOL-sequent`  0
                              THEN  Auto))
              THEN  MoveToConcl  (-1)\mcdot{}
              THEN  MoveToConcl  10
              THEN  (GenConcl  \mkleeneopen{}mFOquant-body(hyps[hypnum])  =  B\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (GenConcl  \mkleeneopen{}mFOquant-var(hyps[hypnum])  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Auto)\mcdot{})

---

Home Index