---

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


1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. hypnum : ℕ@i
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. [Dom] : Type
9. [S] : FOStruct(Dom)
10. a : FOAssignment(Dom)@i
11. Dom,S,a |= mFOL-abstract(hyps[hypnum])@i
⊢ Dom,S,a |= mFOL-abstract(mFOconnect-left(hyps[hypnum]))
BY
{ (Subst ⌈hyps[hypnum] = mFOconnect-left(hyps[hypnum]) ∧ mFOconnect-right(hyps[hypnum]) ∈ mFOL()⌉ (-1)⋅
   THENA (Auto
          THEN 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)
   )⋅ }

1
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. hypnum : ℕ@i
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. [Dom] : Type
9. [S] : FOStruct(Dom)
10. a : FOAssignment(Dom)@i
11. Dom,S,a |= mFOL-abstract(mFOconnect-left(hyps[hypnum]) ∧ mFOconnect-right(hyps[hypnum]))
⊢ Dom,S,a |= mFOL-abstract(mFOconnect-left(hyps[hypnum]))

---

Latex:



1.  hyps  :  mFOL()  List@i
2.  concl  :  mFOL()@i
3.  hypnum  :  \mBbbN{}@i
4.  hypnum  <  ||hyps||
5.  \muparrow{}mFOconnect?(hyps[hypnum])
6.  mFOconnect-knd(hyps[hypnum])  =  "and"
7.  mFOL-sequent-evidence(<[mFOconnect-left(hyps[hypnum]);  [mFOconnect-right(hyps[hypnum])  /  hyps]]
                                                  ,  concl
                                                  >)
8.  [Dom]  :  Type
9.  [S]  :  FOStruct(Dom)
10.  a  :  FOAssignment(Dom)@i
11.  Dom,S,a  |=  mFOL-abstract(hyps[hypnum])@i
\mvdash{}  Dom,S,a  |=  mFOL-abstract(mFOconnect-left(hyps[hypnum]))


By

(Subst  \mkleeneopen{}hyps[hypnum]  =  mFOconnect-left(hyps[hypnum])  \mwedge{}  mFOconnect-right(hyps[hypnum])\mkleeneclose{}  (-1)\mcdot{}
  THENA  (Auto
                THEN  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)
  )\mcdot{}

---

Home Index