---

Step * 1 8 of Lemma FOL-proveable-evidence


1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. subproofs : ℕ||subgoals|| ⟶ proof-tree(mFOL-sequent();FOLRule();λsr.FOLeffect(sr))
5. ∀b:ℕ||subgoals||. ∀s:mFOL-sequent().
     (correct_proof(mFOL-sequent();λsr.FOLeffect(sr);s;subproofs b) ⇒ FOL-sequent-evidence{i:l}(s))
6. ∀i:ℕ||subgoals||. correct_proof(mFOL-sequent();λsr.FOLeffect(sr);subgoals[i];subproofs i)
7. hypnum : ℕ
8. hypnum < ||hyps||
9. ↑mFOconnect?(hyps[hypnum])
10. mFOconnect-knd(hyps[hypnum]) = "and" ∈ Atom
11. [<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>] = subgoals ∈ (mFOL-sequent() Lis\000Ct)
12. FOL-sequent-evidence{i:l}(<[mFOconnect-left(hyps[hypnum]); [mFOconnect-right(hyps[hypnum]) / hyps]], concl>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)
BY
{ (ThinVar `subgoals'
   THEN TACTIC:((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 `FOL-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. FOL-sequent-evidence{i:l}(<[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])
⊢ FOL-sequent-evidence{i:l}(<[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. FOL-sequent-evidence{i:l}(<[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. FOL-sequent-evidence{i:l}(<[mFOconnect-right(hyps[hypnum]) / hyps], concl>)
⊢ FOL-sequent-evidence{i:l}(<hyps, concl>)

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  subgoals  :  mFOL-sequent()  List
4.  subproofs  :  \mBbbN{}||subgoals||  {}\mrightarrow{}  proof-tree(mFOL-sequent();FOLRule();\mlambda{}sr.FOLeffect(sr))
5.  \mforall{}b:\mBbbN{}||subgoals||.  \mforall{}s:mFOL-sequent().
          (correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(sr);s;subproofs  b)  {}\mRightarrow{}  FOL-sequent-evidence\{i:l\}(s))
6.  \mforall{}i:\mBbbN{}||subgoals||.  correct\_proof(mFOL-sequent();\mlambda{}sr.FOLeffect(sr);subgoals[i];subproofs  i)
7.  hypnum  :  \mBbbN{}
8.  hypnum  <  ||hyps||
9.  \muparrow{}mFOconnect?(hyps[hypnum])
10.  mFOconnect-knd(hyps[hypnum])  =  "and"
11.  [<[mFOconnect-left(hyps[hypnum]);  [mFOconnect-right(hyps[hypnum])  /  hyps]],  concl>]  =  subgoals
12.  FOL-sequent-evidence\{i:l\}(<[mFOconnect-left(hyps[hypnum]);
                                                                [mFOconnect-right(hyps[hypnum])  /  hyps]]
                                                            ,  concl
                                                            >)
\mvdash{}  FOL-sequent-evidence\{i:l\}(<hyps,  concl>)


By

---

Latex:
(ThinVar  `subgoals'
  THEN  TACTIC:((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  `FOL-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