---

Step * 1 2 1 1 1 8 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. hypnum < ||hyps||
7. ↑mFOconnect?(hyps[hypnum])
8. mFOconnect-knd(hyps[hypnum]) = "and" ∈ Atom
9. [<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>] = subgoals ∈ (mFOL-sequent() List\000C)
10. mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>)
⊢ mFOL-sequent-evidence(<hyps, concl>)
BY
{ (ThinVar `subgoals'
   THEN (Assert hyps[hypnum] = mFOconnect-left(hyps[hypnum]) ∧ mFOconnect-right(hyps[hypnum]) ∈ mFOL() BY
               (Auto
                THEN RepeatFor 2 (MoveToConcl (-2))
                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 (Assert mFOL-freevars(mFOconnect-left(hyps[hypnum])) ⊆ mFOL-freevars(hyps[hypnum]) BY
               ((Assert mFOL-freevars(mFOconnect-left(hyps[hypnum]))
                        ⊆ mFOL-freevars(mFOconnect-left(hyps[hypnum]) ∧ mFOconnect-right(hyps[hypnum])) BY
                       Auto)
                THEN Auto
                ))
   THEN FLemma `mFOL-sequent-evidence_transitivity2` [-3]
   THEN Auto
   THEN Try ((Using [`B', ⌜mFOL-freevars(hyps[hypnum])⌝] (BLemma `l_contains_transitivity`)⋅ THEN EAuto 1))) }

1
.....antecedent..... 
1. hyps : mFOL() List
2. concl : mFOL()
3. hypnum : ℕ
4. hypnum < ||hyps||
5. ↑mFOconnect?(hyps[hypnum])
6. mFOconnect-knd(hyps[hypnum]) = "and" ∈ Atom
7. mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>)
8. hyps[hypnum] = mFOconnect-left(hyps[hypnum]) ∧ mFOconnect-right(hyps[hypnum]) ∈ mFOL()
9. mFOL-freevars(mFOconnect-left(hyps[hypnum])) ⊆ mFOL-freevars(hyps[hypnum])
⊢ mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum]) / hyps], mFOconnect-left(hyps[hypnum])>)

2
1. hyps : mFOL() List
2. concl : mFOL()
3. hypnum : ℕ
4. hypnum < ||hyps||
5. ↑mFOconnect?(hyps[hypnum])
6. mFOconnect-knd(hyps[hypnum]) = "and" ∈ Atom
7. mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>)
8. hyps[hypnum] = mFOconnect-left(hyps[hypnum]) ∧ mFOconnect-right(hyps[hypnum]) ∈ mFOL()
9. mFOL-freevars(mFOconnect-left(hyps[hypnum])) ⊆ mFOL-freevars(hyps[hypnum])
10. mFOL-sequent-evidence(<[mFOconnect-right(hyps[hypnum]) / hyps], concl>)
⊢ mFOL-sequent-evidence(<hyps, 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.  hypnum  <  ||hyps||
7.  \muparrow{}mFOconnect?(hyps[hypnum])
8.  mFOconnect-knd(hyps[hypnum])  =  "and"
9.  [<[mFOconnect-left(hyps[hypnum]);  [mFOconnect-right(hyps[hypnum])  /  hyps]],  concl>]  =  subgoals
10.  mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]);  [mFOconnect-right(hyps[hypnum])  /  hyps]]
                                                    ,  concl
                                                    >)
\mvdash{}  mFOL-sequent-evidence(<hyps,  concl>)


By

---

Latex:
(ThinVar  `subgoals'
  THEN  (Assert  hyps[hypnum]  =  mFOconnect-left(hyps[hypnum])  \mwedge{}  mFOconnect-right(hyps[hypnum])  BY
                          (Auto
                            THEN  RepeatFor  2  (MoveToConcl  (-2))
                            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  (Assert  mFOL-freevars(mFOconnect-left(hyps[hypnum]))  \msubseteq{}  mFOL-freevars(hyps[hypnum])  BY
                          ((Assert  mFOL-freevars(mFOconnect-left(hyps[hypnum]))
                                            \msubseteq{}  mFOL-freevars(mFOconnect-left(hyps[hypnum])  \mwedge{}
                                                                            mFOconnect-right(hyps[hypnum]))  BY
                                          Auto)
                            THEN  Auto
                            ))
  THEN  FLemma  `mFOL-sequent-evidence\_transitivity2`  [-3]
  THEN  Auto
  THEN  Try  ((Using  [`B',  \mkleeneopen{}mFOL-freevars(hyps[hypnum])\mkleeneclose{}]  (BLemma  `l\_contains\_transitivity`)\mcdot{}
                        THEN  EAuto  1
                        )))

---

Home Index