---

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


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

---

Latex:



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


By

(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  11
              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{})\mcdot{}

---

Home Index