---

Step * of Lemma State1-prior

∀[Info,A,B:Type]. ∀[init:Id ─→ B]. ∀[f:Id ─→ A ─→ B ─→ B]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  (Prior(State1(init;f;X))?λloc.{init loc}(e)
  = if first(e) then {init loc(e)} else State1(init;f;X)(pred(e)) fi 
  ∈ bag(B))
BY
{ (Auto
   THEN RepUR ``primed-class-opt class-ap`` 0
   THEN Fold `class-ap` 0
   THEN GenConclAtAddr [2;1]
   THEN DProdsAndUnions
   THEN AllReduce
   THEN Thin (-1)
   THEN AutoSplit) }

1
1. Info : Type
2. A : Type
3. B : Type
4. init : Id ─→ B
5. f : Id ─→ A ─→ B ─→ B
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. ¬↑first(e)
10. x : E@i
11. (x <loc e)@i
12. ↑0 <z #(State1(init;f;X)(x))@i
13. ∀e'':E. ((x <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(State1(init;f;X)(e''))))@i
⊢ State1(init;f;X)(x) = State1(init;f;X)(pred(e)) ∈ bag(B)

2
1. Info : Type
2. A : Type
3. B : Type
4. init : Id ─→ B
5. f : Id ─→ A ─→ B ─→ B
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. ¬↑first(e)
10. y : ¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(State1(init;f;X)(e'))))})@i
⊢ {init loc(e)} = State1(init;f;X)(pred(e)) ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[f:Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (Prior(State1(init;f;X))?\mlambda{}loc.\{init  loc\}(e)
    =  if  first(e)  then  \{init  loc(e)\}  else  State1(init;f;X)(pred(e))  fi  )


By

---

Latex:
(Auto
  THEN  RepUR  ``primed-class-opt  class-ap``  0
  THEN  Fold  `class-ap`  0
  THEN  GenConclAtAddr  [2;1]
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  Thin  (-1)
  THEN  AutoSplit)

---

Home Index