---

Step * 1 9 1 1 1 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]) = "or" ∈ Atom
8. hyps[hypnum] = mFOconnect-left(hyps[hypnum]) ∨ mFOconnect-right(hyps[hypnum]) ∈ mFOL()
9. [Dom] : Type
10. [S] : FOStruct(Dom)
11. a : FOAssignment(Dom)@i
12. f : tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);[mFOconnect-left(hyps[hypnum]) / hyps]))
─→ Dom,S,a |= mFOL-abstract(concl)
13. g : tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);[mFOconnect-right(hyps[hypnum]) / hyps]))
─→ Dom,S,a |= mFOL-abstract(concl)
⊢ tuple-type(map(λh.Dom,S,a |= mFOL-abstract(h);hyps)) ─→ Dom,S,a |= mFOL-abstract(concl)
BY
{ (UseWitness ⌈λx.case x.hypnum of inl(a) => f <a, x> | inr(b) => g <b, x>⌉⋅
   THEN Auto
   THEN GenConclAtAddr [2;1]
   THEN Thin (-1)
   THEN (RWO "select-map" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN (HypSubst' 8 -1 THENA Auto)
   THEN (RepUR ``mFOL-abstract`` (-1)
         THEN Fold `mFOL-abstract` (-1)
         THEN RepUR ``FOConnective FOSatWith let`` (-1)
         THEN All (Fold `FOSatWith`)
         THEN Auto
         THEN Reduce 0
         THEN AutoSplit
         THEN (DVar `hyps' THEN All Reduce THEN Auto')⋅)⋅)⋅ }

---

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])  =  "or"
8.  hyps[hypnum]  =  mFOconnect-left(hyps[hypnum])  \mvee{}  mFOconnect-right(hyps[hypnum])
9.  [Dom]  :  Type
10.  [S]  :  FOStruct(Dom)
11.  a  :  FOAssignment(Dom)@i
12.  f  :  tuple-type(map(\mlambda{}h.Dom,S,a  |=  mFOL-abstract(h);[mFOconnect-left(hyps[hypnum])  /  hyps]))
{}\mrightarrow{}  Dom,S,a  |=  mFOL-abstract(concl)
13.  g  :  tuple-type(map(\mlambda{}h.Dom,S,a  |=  mFOL-abstract(h);[mFOconnect-right(hyps[hypnum])  /  hyps]))
{}\mrightarrow{}  Dom,S,a  |=  mFOL-abstract(concl)
\mvdash{}  tuple-type(map(\mlambda{}h.Dom,S,a  |=  mFOL-abstract(h);hyps))  {}\mrightarrow{}  Dom,S,a  |=  mFOL-abstract(concl)


By

(UseWitness  \mkleeneopen{}\mlambda{}x.case  x.hypnum  of  inl(a)  =>  f  <a,  x>  |  inr(b)  =>  g  <b,  x>\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  GenConclAtAddr  [2;1]
  THEN  Thin  (-1)
  THEN  (RWO  "select-map"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  (HypSubst'  8  -1  THENA  Auto)
  THEN  (RepUR  ``mFOL-abstract``  (-1)
              THEN  Fold  `mFOL-abstract`  (-1)
              THEN  RepUR  ``FOConnective  FOSatWith  let``  (-1)
              THEN  All  (Fold  `FOSatWith`)
              THEN  Auto
              THEN  Reduce  0
              THEN  AutoSplit
              THEN  (DVar  `hyps'  THEN  All  Reduce  THEN  Auto')\mcdot{})\mcdot{})\mcdot{}

---

Home Index