---

Step * 4 1 of Lemma State-comb-fun-eq


1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. ¬↑first(e)
10. ¬↑e ∈b X
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. (X es e) = {} ∈ bag(A)
⊢ sv-bag-only(Prior(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init))?init es e)
= sv-bag-only(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es pred(e))
∈ B
BY
{ ((Subst ⌈rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) ~ State-comb(init;f;X)\000C⌉ 0⋅
    THENA (RepUR ``State-comb rec-combined-class-opt-1`` 0 THEN Auto)
    )
   THEN RepUR ``primed-class-opt`` 0
   THEN (GenConclAtAddr [2;1;1] THENA (Reduce 0 THEN RepeatFor 2 (MaAuto)))) }

1
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. ¬↑first(e)
10. ¬↑e ∈b X
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. (X es e) = {} ∈ bag(A)
15. v : (∃e':{E| ((e' <loc e)
                 ∧ (↑((λe'.0 <z #(State-comb(init;f;X) es e')) e'))
                 ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑((λe'.0 <z #(State-comb(init;f;X) es e')) e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(State-comb(init;f;X) es e')) e')))}))@i
16. (last(λe'.0 <z #(State-comb(init;f;X) es e')) e)
= v
∈ ((∃e':{E| ((e' <loc e)
            ∧ (↑((λe'.0 <z #(State-comb(init;f;X) es e')) e'))
            ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑((λe'.0 <z #(State-comb(init;f;X) es e')) e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(State-comb(init;f;X) es e')) e')))})))@i
⊢ sv-bag-only(case v of inl(e') => State-comb(init;f;X) es e' | inr(x) => init loc(e))
= sv-bag-only(State-comb(init;f;X) es pred(e))
∈ B

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  A  :  Type
4.  f  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B
5.  init  :  Id  {}\mrightarrow{}  bag(B)
6.  X  :  EClass(A)
7.  es  :  EO+(Info)
8.  e  :  E
9.  \mneg{}\muparrow{}first(e)
10.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  X
11.  \mforall{}l:Id.  (1  \mleq{}  \#(init  l))
12.  \mforall{}l:Id.  single-valued-bag(init  l;B)
13.  single-valued-classrel(es;X;A)
14.  (X  es  e)  =  \{\}
\mvdash{}  sv-bag-only(Prior(rec-comb(\mlambda{}n.[X][n];\mlambda{}i,w,s.  if  bag-null(w  0)
                                                                                            then  s
                                                                                            else  lifting-2(f)  (w  0)  s
                                                                                            fi  ;init))?init 
                            es 
                            e)
=  sv-bag-only(rec-comb(\mlambda{}n.[X][n];\mlambda{}i,w,s.  if  bag-null(w  0)  then  s  else  lifting-2(f)  (w  0)  s  fi  ;init)\000C  es 
                            pred(e))


By

---

Latex:
((Subst  \mkleeneopen{}rec-comb(\mlambda{}n.[X][n];\mlambda{}i,w,s.  if  bag-null(w  0)  then  s  else  lifting-2(f)  (w  0)  s  fi  ;init) 
                  \msim{}  State-comb(init;f;X)\mkleeneclose{}  0\mcdot{}
    THENA  (RepUR  ``State-comb  rec-combined-class-opt-1``  0  THEN  Auto)
    )
  THEN  RepUR  ``primed-class-opt``  0
  THEN  (GenConclAtAddr  [2;1;1]  THENA  (Reduce  0  THEN  RepeatFor  2  (MaAuto))))

---

Home Index