---

Step * 1 10 1 2 of Lemma mFOL-proveable-evidence


1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. hypnum : ℕ@i
5. hypnum < ||hyps||
6. ↑mFOconnect?(hyps[hypnum])
7. mFOconnect-knd(hyps[hypnum]) = "imp" ∈ Atom
8. mFOL-sequent-evidence(<hyps, mFOconnect-left(hyps[hypnum])>)
⊢ mFOL-sequent-evidence(<hyps
                        , mFOconnect-left(hyps[hypnum]) ⇒ mFOconnect-right(hyps[hypnum]) ∧
                          mFOconnect-left(hyps[hypnum])
                        >)
BY
{ ((Assert hyps[hypnum] = mFOconnect-left(hyps[hypnum]) ⇒ mFOconnect-right(hyps[hypnum]) ∈ mFOL() BY
          (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 RevHypSubst (-1) 0
   THEN Auto
   THEN Try ((Unfold `mFOL-sequent` 0 THEN Auto)))⋅ }

1
1. hyps : mFOL() List@i
2. concl : mFOL()@i
3. subgoals : mFOL-sequent() List@i
4. hypnum : ℕ@i
5. hypnum < ||hyps||
6. ↑mFOconnect?(hyps[hypnum])
7. mFOconnect-knd(hyps[hypnum]) = "imp" ∈ Atom
8. mFOL-sequent-evidence(<hyps, mFOconnect-left(hyps[hypnum])>)
9. hyps[hypnum] = mFOconnect-left(hyps[hypnum]) ⇒ mFOconnect-right(hyps[hypnum]) ∈ mFOL()
⊢ mFOL-sequent-evidence(<hyps, hyps[hypnum] ∧ mFOconnect-left(hyps[hypnum])>)

---

Latex:



1.  hyps  :  mFOL()  List@i
2.  concl  :  mFOL()@i
3.  subgoals  :  mFOL-sequent()  List@i
4.  hypnum  :  \mBbbN{}@i
5.  hypnum  <  ||hyps||
6.  \muparrow{}mFOconnect?(hyps[hypnum])
7.  mFOconnect-knd(hyps[hypnum])  =  "imp"
8.  mFOL-sequent-evidence(<hyps,  mFOconnect-left(hyps[hypnum])>)
\mvdash{}  mFOL-sequent-evidence(<hyps
                                                ,  mFOconnect-left(hyps[hypnum])  {}\mRightarrow{}  mFOconnect-right(hyps[hypnum])  \mwedge{}
                                                    mFOconnect-left(hyps[hypnum])
                                                >)


By

((Assert  hyps[hypnum]  =  mFOconnect-left(hyps[hypnum])  {}\mRightarrow{}  mFOconnect-right(hyps[hypnum])  BY
                (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))\mcdot{}
  THEN  RevHypSubst  (-1)  0
  THEN  Auto
  THEN  Try  ((Unfold  `mFOL-sequent`  0  THEN  Auto)))\mcdot{}

---

Home Index