Step
*
2
of Lemma
loop-class-state-fun-eq
1. Info : Type
2. B : Type
3. init : Id ─→ bag(B)
4. X : EClass(B ─→ B)
5. es : EO+(Info)
6. e : E
7. ¬↑first(e)
8. ∀l:Id. (1 ≤ #(init l))
9. single-valued-classrel(es;X;B ─→ B)
10. ∀l:Id. single-valued-bag(init l;B)
11. ↑e ∈b X
⊢ loop-class-state(X;init)(e) = (X@e loop-class-state(X;init)(pred(e))) ∈ B
BY
{ (RW (AddrC [2;2] (RecUnfoldC `loop-class-state`)) 0
THEN RepUR ``eclass-cond classfun`` 0
THEN AutoSplit
THEN RepUR ``eclass3 class-ap`` 0
THEN (RWO "primed-class-opt-cases" 0 THENA (Try (Complete (Auto)) THEN DoSubsume THEN Auto))
THEN Repeat (AutoSplit)) }
1
1. Info : Type
2. B : Type
3. init : Id ─→ bag(B)
4. X : EClass(B ─→ B)
5. es : EO+(Info)
6. e : E
7. ¬↑first(e)
8. ¬False
9. ∀l:Id. (1 ≤ #(init l))
10. single-valued-classrel(es;X;B ─→ B)
11. ∀l:Id. single-valued-bag(init l;B)
12. ↑e ∈b X
13. ↑e ∈b X
14. 0 < #(loop-class-state(X;init) es pred(e))
⊢ sv-bag-only(∪f∈X es e.bag-map(f;loop-class-state(X;init) es pred(e)))
= (X@e sv-bag-only(loop-class-state(X;init) es pred(e)))
∈ B
2
1. Info : Type
2. B : Type
3. init : Id ─→ bag(B)
4. X : EClass(B ─→ B)
5. es : EO+(Info)
6. e : E
7. ¬0 < #(loop-class-state(X;init) es pred(e))
8. ¬↑first(e)
9. ¬False
10. ∀l:Id. (1 ≤ #(init l))
11. single-valued-classrel(es;X;B ─→ B)
12. ∀l:Id. single-valued-bag(init l;B)
13. ↑e ∈b X
14. ↑e ∈b X
⊢ sv-bag-only(∪f∈X es e.bag-map(f;Prior(loop-class-state(X;init))?init es pred(e)))
= (X@e sv-bag-only(loop-class-state(X;init) es pred(e)))
∈ B
Latex:
Latex:
1. Info : Type
2. B : Type
3. init : Id {}\mrightarrow{} bag(B)
4. X : EClass(B {}\mrightarrow{} B)
5. es : EO+(Info)
6. e : E
7. \mneg{}\muparrow{}first(e)
8. \mforall{}l:Id. (1 \mleq{} \#(init l))
9. single-valued-classrel(es;X;B {}\mrightarrow{} B)
10. \mforall{}l:Id. single-valued-bag(init l;B)
11. \muparrow{}e \mmember{}\msubb{} X
\mvdash{} loop-class-state(X;init)(e) = (X@e loop-class-state(X;init)(pred(e)))
By
Latex:
(RW (AddrC [2;2] (RecUnfoldC `loop-class-state`)) 0
THEN RepUR ``eclass-cond classfun`` 0
THEN AutoSplit
THEN RepUR ``eclass3 class-ap`` 0
THEN (RWO "primed-class-opt-cases" 0 THENA (Try (Complete (Auto)) THEN DoSubsume THEN Auto))
THEN Repeat (AutoSplit))
Home
Index