---

Step * 1 of Lemma State1-prior


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)
BY
{ (InstLemma `es-pred_property` [⌈es⌉;⌈e⌉]⋅
   THEN Auto
   THEN (InstHyp [⌈x⌉] (-1)⋅ THENA Auto)
   THEN DProdsAndUnions
   THEN Auto
   THEN Assert ⌈False⌉⋅
   THEN Auto
   THEN (InstHyp [⌈pred(e)⌉] (-5)⋅ THEN MaAuto)
   THEN D (-1)
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (BLemma `bag-size-bag-member` THENA Auto)
   THEN RepUR ``class-ap`` 0
   THEN Fold `classrel` 0
   THEN BLemma `State1-loc-exists`
   THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  init  :  Id  {}\mrightarrow{}  B
5.  f  :  Id  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
6.  X  :  EClass(A)
7.  es  :  EO+(Info)
8.  e  :  E
9.  \mneg{}\muparrow{}first(e)
10.  x  :  E@i
11.  (x  <loc  e)@i
12.  \muparrow{}0  <z  \#(State1(init;f;X)(x))@i
13.  \mforall{}e'':E.  ((x  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}0  <z  \#(State1(init;f;X)(e''))))@i
\mvdash{}  State1(init;f;X)(x)  =  State1(init;f;X)(pred(e))


By

---

Latex:
(InstLemma  `es-pred\_property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  DProdsAndUnions
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  (-5)\mcdot{}  THEN  MaAuto)
  THEN  D  (-1)
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (BLemma  `bag-size-bag-member`  THENA  Auto)
  THEN  RepUR  ``class-ap``  0
  THEN  Fold  `classrel`  0
  THEN  BLemma  `State1-loc-exists`
  THEN  Auto)

---

Home Index