---

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


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
((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  `FOL-sequent`  0  THEN  Auto)))\mcdot{}

---

Home Index