---

Step * 1 11 1 2 2 2 1 of Lemma FOL-proveable-evidence


1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. var : ℤ
6. hypnum < ||hyps||
7. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. ∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
      ∀a:FOAssignment(mFOL-sequent-freevars(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps]
                                            , concl
                                            >),Dom)
        Dom,S,a +|= FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
11. hyps[hypnum] = ∀mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum])) ∈ mFOL()
12. mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum]) ⊆ mFOL-sequent-freevars(<hyps
                                                        , mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]
                                                        >)
14. ¬(mFOquant-var(hyps[hypnum]) ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
= FOL-abstract(mFOquant-body(hyps[hypnum]))
∈ AbstractFOFormula+(mFOL-freevars(mFOquant-body(hyps[hypnum])))
16. [Dom] : Type
17. [S] : FOStruct+{i:l}(Dom)
18. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
19. Dom,S,a +|= FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
⊢ Dom,S,a +|= FOL-sequent-abstract(<hyps, concl>)
BY
{ (RepUR ``FOL-sequent-abstract FOSatWith+`` 0
   THEN RepUR ``FOL-sequent-abstract FOSatWith+`` -1
   THEN Fold `FOSatWith+` (-1)⋅
   THEN Fold `FOSatWith+` 0⋅
   THEN Fold `implies` (-1)
   THEN Fold `implies` 0
   THEN ParallelLast) }

1
.....antecedent..... 
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. var : ℤ
6. hypnum < ||hyps||
7. (var ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. ∀[Dom:Type]. ∀[S:FOStruct+{i:l}(Dom)].
      ∀a:FOAssignment(mFOL-sequent-freevars(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps]
                                            , concl
                                            >),Dom)
        Dom,S,a +|= FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps], concl>)
11. hyps[hypnum] = ∀mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum])) ∈ mFOL()
12. mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum]) ⊆ mFOL-sequent-freevars(<hyps
                                                        , mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]
                                                        >)
14. ¬(mFOquant-var(hyps[hypnum]) ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
= FOL-abstract(mFOquant-body(hyps[hypnum]))
∈ AbstractFOFormula+(mFOL-freevars(mFOquant-body(hyps[hypnum])))
16. [Dom] : Type
17. [S] : FOStruct+{i:l}(Dom)
18. a : FOAssignment(mFOL-sequent-freevars(<hyps, concl>),Dom)
19. tuple-type(FOL-hyps-meaning(Dom;S;a;hyps))
⊢ tuple-type(FOL-hyps-meaning(Dom;S;a;[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])] / hyps]))

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  subgoals  :  mFOL-sequent()  List
4.  hypnum  :  \mBbbN{}
5.  var  :  \mBbbZ{}
6.  hypnum  <  ||hyps||
7.  (var  \mmember{}  mFOL-sequent-freevars(<hyps,  concl>))
8.  \muparrow{}mFOquant?(hyps[hypnum])
9.  mFOquant-isall(hyps[hypnum])  =  tt
10.  \mforall{}[Dom:Type].  \mforall{}[S:FOStruct+\{i:l\}(Dom)].
            \mforall{}a:FOAssignment(mFOL-sequent-freevars(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(...)]  / 
                                                                                            hyps]
                                                                                        ,  concl
                                                                                        >),Dom)
                Dom,S,a  +|=  FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(...)]  / 
                                                                                      hyps]
                                                                                  ,  concl
                                                                                  >)
11.  hyps[hypnum]  =  \mforall{}mFOquant-var(hyps[hypnum]);mFOquant-body(hyps[hypnum]))
12.  mFOL-freevars(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
        \msubseteq{}  mFOL-sequent-freevars(<hyps,  concl>)
13.  mFOL-freevars(hyps[hypnum])
        \msubseteq{}  mFOL-sequent-freevars(<hyps,  mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])]>)
14.  \mneg{}(mFOquant-var(hyps[hypnum])  \mmember{}  mFOL-freevars(mFOquant-body(hyps[hypnum])))
15.  FOL-abstract(mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[hypnum])])
=  FOL-abstract(mFOquant-body(hyps[hypnum]))
16.  [Dom]  :  Type
17.  [S]  :  FOStruct+\{i:l\}(Dom)
18.  a  :  FOAssignment(mFOL-sequent-freevars(<hyps,  concl>),Dom)
19.  Dom,S,a  +|=  FOL-sequent-abstract(<[mFOquant-body(hyps[hypnum])[var/mFOquant-var(hyps[...])]  / 
                                                                              hyps]
                                                                          ,  concl
                                                                          >)
\mvdash{}  Dom,S,a  +|=  FOL-sequent-abstract(<hyps,  concl>)


By

---

Latex:
(RepUR  ``FOL-sequent-abstract  FOSatWith+``  0
  THEN  RepUR  ``FOL-sequent-abstract  FOSatWith+``  -1
  THEN  Fold  `FOSatWith+`  (-1)\mcdot{}
  THEN  Fold  `FOSatWith+`  0\mcdot{}
  THEN  Fold  `implies`  (-1)
  THEN  Fold  `implies`  0
  THEN  ParallelLast)

---

Home Index