---

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


1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. x : ℤ
6. hypnum < ||hyps||
7. (x ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. FOL-sequent-evidence{i:l}(<[mFOquant-body(hyps[hypnum])[x/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])[x/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum]) ⊆ mFOL-sequent-freevars(<hyps
                                                        , mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]
                                                        >)
14. (mFOquant-var(hyps[hypnum]) ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. [Dom] : Type
16. [S] : FOStruct+{i:l}(Dom)
17. a : FOAssignment(mFOL-sequent-freevars(<hyps, mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]>),Dom)
18. (∀v:Dom. Dom,S,a[mFOquant-var(hyps[hypnum]) := v] +|= FOL-abstract(mFOquant-body(hyps[hypnum]))) ⋃ (S "false" [])
⊢ Dom,S,a +|= FOL-abstract(mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])])
BY
{ Assert ⌜(x ∈ mFOL-sequent-freevars(<hyps, mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]>))⌝⋅ }

1
.....assertion..... 
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. x : ℤ
6. hypnum < ||hyps||
7. (x ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. FOL-sequent-evidence{i:l}(<[mFOquant-body(hyps[hypnum])[x/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])[x/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum]) ⊆ mFOL-sequent-freevars(<hyps
                                                        , mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]
                                                        >)
14. (mFOquant-var(hyps[hypnum]) ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. [Dom] : Type
16. [S] : FOStruct+{i:l}(Dom)
17. a : FOAssignment(mFOL-sequent-freevars(<hyps, mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]>),Dom)
18. (∀v:Dom. Dom,S,a[mFOquant-var(hyps[hypnum]) := v] +|= FOL-abstract(mFOquant-body(hyps[hypnum]))) ⋃ (S "false" [])
⊢ (x ∈ mFOL-sequent-freevars(<hyps, mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]>))

2
1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. hypnum : ℕ
5. x : ℤ
6. hypnum < ||hyps||
7. (x ∈ mFOL-sequent-freevars(<hyps, concl>))
8. ↑mFOquant?(hyps[hypnum])
9. mFOquant-isall(hyps[hypnum]) = tt
10. FOL-sequent-evidence{i:l}(<[mFOquant-body(hyps[hypnum])[x/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])[x/mFOquant-var(hyps[hypnum])]) ⊆ mFOL-sequent-freevars(<hyps, concl>)
13. mFOL-freevars(hyps[hypnum]) ⊆ mFOL-sequent-freevars(<hyps
                                                        , mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]
                                                        >)
14. (mFOquant-var(hyps[hypnum]) ∈ mFOL-freevars(mFOquant-body(hyps[hypnum])))
15. [Dom] : Type
16. [S] : FOStruct+{i:l}(Dom)
17. a : FOAssignment(mFOL-sequent-freevars(<hyps, mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]>),Dom)
18. (∀v:Dom. Dom,S,a[mFOquant-var(hyps[hypnum]) := v] +|= FOL-abstract(mFOquant-body(hyps[hypnum]))) ⋃ (S "false" [])
19. (x ∈ mFOL-sequent-freevars(<hyps, mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]>))
⊢ Dom,S,a +|= FOL-abstract(mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])])

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}(x  \mmember{}  mFOL-sequent-freevars(<hyps,  mFOquant-body(hyps[hypnum])[x/mFOquant-var(hyps[hypnum])]>\000C))\mkleeneclose{}\mcdot{}

---

Home Index