---

Step * of Lemma rec-combined-loc-class-opt-1-single-val0

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[F:Id ⟶ A ⟶ B ⟶ B]. ∀[X:EClass(A)]. ∀[init:Id ⟶ bag(B)]. ∀[e:E]. ∀[v1,v2:B].
  (v1 = v2 ∈ B) supposing 
     (v1 ∈ lifting-loc-2(F)|Loc, X, Prior(self)?init|(e) and 
     v2 ∈ lifting-loc-2(F)|Loc, X, Prior(self)?init|(e) and 
     single-valued-classrel(es;X;A) and 
     single-valued-bag(init loc(e);B))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 7 (MoveToConcl (-1))
   THEN VrCausalInd'
   THEN Auto
   THEN RepeatFor 2 (MaUseClassRel (-2))
   THEN RepeatFor 2 (MaUseClassRel (-1))
   THEN (HypSubst' (-6) 0 THENA Auto)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN UseSingleVal (-8) (-3)
   THEN (RevHypSubst' (-1) 0 THENA Auto)
   THEN MemCD
   THEN Auto
   THEN MaUseClassRel (-8)
   THEN MaUseClassRel (-3)
   THEN All (RepUR ``es-p-local-pred``)
   THEN RepD
   THEN Try (Complete ((UseSingleVal (-9) (-3) THEN Auto)))
   THEN Try (Complete ((Assert ⌜False⌝⋅ THEN Auto)))
   THEN UseLoclTri ⌜es⌝⌜e'⌝⌜e1⌝⋅
   THEN (Assert ⌜False⌝⋅ THEN Auto)
   THEN ((InstHyp [⌜e1⌝] (-14)⋅ THENA Complete (Auto)) ORELSE (InstHyp [⌜e'⌝] (-5)⋅ THENA Complete (Auto)))
   THEN D (-1)
   THEN D 0
   THEN MaAuto) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[F:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].
\mforall{}[e:E].  \mforall{}[v1,v2:B].
    (v1  =  v2)  supposing 
          (v1  \mmember{}  lifting-loc-2(F)|Loc,  X,  Prior(self)?init|(e)  and 
          v2  \mmember{}  lifting-loc-2(F)|Loc,  X,  Prior(self)?init|(e)  and 
          single-valued-classrel(es;X;A)  and 
          single-valued-bag(init  loc(e);B))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  7  (MoveToConcl  (-1))
  THEN  VrCausalInd'
  THEN  Auto
  THEN  RepeatFor  2  (MaUseClassRel  (-2))
  THEN  RepeatFor  2  (MaUseClassRel  (-1))
  THEN  (HypSubst'  (-6)  0  THENA  Auto)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  UseSingleVal  (-8)  (-3)
  THEN  (RevHypSubst'  (-1)  0  THENA  Auto)
  THEN  MemCD
  THEN  Auto
  THEN  MaUseClassRel  (-8)
  THEN  MaUseClassRel  (-3)
  THEN  All  (RepUR  ``es-p-local-pred``)
  THEN  RepD
  THEN  Try  (Complete  ((UseSingleVal  (-9)  (-3)  THEN  Auto)))
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e'\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mcdot{}
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  ((InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-14)\mcdot{}  THENA  Complete  (Auto))
  ORELSE  (InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-5)\mcdot{}  THENA  Complete  (Auto))
  )
  THEN  D  (-1)
  THEN  D  0
  THEN  MaAuto)

---

Home Index