---

Step * of Lemma iterated-classrel-single-val

∀[Info,A,S:Type]. ∀[init:Id ─→ bag(S)]. ∀[f:A ─→ S ─→ S]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v1,v2:S].
  (v1 = v2 ∈ S) supposing 
     (iterated-classrel(es;S;A;f;init;X;e;v2) and 
     iterated-classrel(es;S;A;f;init;X;e;v1) and 
     single-valued-bag(init loc(e);S) and 
     single-valued-classrel(es;X;A))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 7 (MoveToConcl (-1))
   THEN StrongCausalInd
   THEN (UnivCD THENA Auto)
   THEN RecUnfold `iterated-classrel` (-1)
   THEN RecUnfold `iterated-classrel` (-2)
   THEN ExRepD
   THEN (SplitOnHypITE  (-5) THENA Auto)
   THEN (SplitOnHypITE  (-3) THENA Auto)
   THEN Auto
   THEN (UseSingleVal (-7) (-4) ORELSE (InstHyp [⌈pred(e)⌉;⌈z1⌉;⌈z⌉] (-13)⋅ THENA Auto))
   THEN SplitOrHyps
   THEN ExRepD
   THEN Auto
   THEN Try (Complete ((Assert ⌈False⌉⋅ THEN Auto)))
   THEN UseSingleVal (-10) (-5)
   THEN Auto) }

---

Latex:


\mforall{}[Info,A,S:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(S)].  \mforall{}[f:A  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
\mforall{}[v1,v2:S].
    (v1  =  v2)  supposing 
          (iterated-classrel(es;S;A;f;init;X;e;v2)  and 
          iterated-classrel(es;S;A;f;init;X;e;v1)  and 
          single-valued-bag(init  loc(e);S)  and 
          single-valued-classrel(es;X;A))


By

((UnivCD  THENA  Auto)
  THEN  RepeatFor  7  (MoveToConcl  (-1))
  THEN  StrongCausalInd
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `iterated-classrel`  (-1)
  THEN  RecUnfold  `iterated-classrel`  (-2)
  THEN  ExRepD
  THEN  (SplitOnHypITE    (-5)  THENA  Auto)
  THEN  (SplitOnHypITE    (-3)  THENA  Auto)
  THEN  Auto
  THEN  (UseSingleVal  (-7)  (-4)  ORELSE  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  (-13)\mcdot{}  THENA  Auto))
  THEN  SplitOrHyps
  THEN  ExRepD
  THEN  Auto
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  UseSingleVal  (-10)  (-5)
  THEN  Auto)

---

Home Index