Step
*
1
2
2
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. ¬((X es e) = {} ∈ bag(A))
10. ∀l:Id. (1 ≤ #(init l))
11. ∀l:Id. single-valued-bag(init l;B)
12. single-valued-classrel(es;X;A)
13. ↑e ∈b X
14. ↑first(e)
15. v : (∃e':{E| ((e' <loc e)
∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init)\000C es
e'))
e'))
∧ (∀e'':E
((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑((λe'.0 <z #(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
e'))
e'')))))})
∨ (¬(∃e':{E| ((e' <loc e)
∧ (↑((λe'.0 <z #(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 \000Ce'))
e')))}))@i
16. (last(λe'.0 <z #(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 e')) e)
= v
∈ ((∃e':{E| ((e' <loc e)
∧ (↑((λe'.0 <z #(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 e\000C'))
e'))
∧ (∀e'':E
((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;ini\000Ct) es
e'))
e'')))))})
∨ (¬(∃e':{E| ((e' <loc e)
∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) e\000Cs
e'))
e')))})))@i
⊢ sv-bag-only(lifting-2(f) (X es e)
case v
of inl(e') =>
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 e'
| inr(x) =>
init loc(e))
= (f sv-bag-only(X es e) sv-bag-only(init loc(e)))
∈ B
BY
{ (All Reduce
THEN DVar `v'
THEN All Reduce
THEN Try (Complete (((Assert ⌈False⌉⋅ THEN Auto) THEN DVar `x' THEN RepD THEN 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. ¬((X es e) = {} ∈ bag(A))
10. ∀l:Id. (1 ≤ #(init l))
11. ∀l:Id. single-valued-bag(init l;B)
12. single-valued-classrel(es;X;A)
13. ↑e ∈b X
14. ↑first(e)
15. y : ¬(∃e':{E| ((e' <loc e)
∧ (↑0 <z #(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
e')))})@i
16. (last(λe'.0 <z #(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 e')) e)
= (inr y )
∈ ((∃e':{E| ((e' <loc e)
∧ (↑0 <z #(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 e'))
∧ (∀e'':E
((e' <loc e'')
⇒ (e'' <loc e)
⇒ (¬↑0 <z #(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
e'')))))})
∨ (¬(∃e':{E| ((e' <loc e)
∧ (↑0 <z #(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
e')))})))@i
⊢ sv-bag-only(lifting-2(f) (X es e) (init loc(e))) = (f sv-bag-only(X es e) sv-bag-only(init loc(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{}((X es e) = \{\})
10. \mforall{}l:Id. (1 \mleq{} \#(init l))
11. \mforall{}l:Id. single-valued-bag(init l;B)
12. single-valued-classrel(es;X;A)
13. \muparrow{}e \mmember{}\msubb{} X
14. \muparrow{}first(e)
15. v : (\mexists{}e':\{E| ((e' <loc e)
\mwedge{} (\muparrow{}((\mlambda{}e'.0 <z \#(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)
es
e'))
e'))
\mwedge{} (\mforall{}e'':E
((e' <loc e'')
{}\mRightarrow{} (e'' <loc e)
{}\mRightarrow{} (\mneg{}\muparrow{}((\mlambda{}e'.0 <z \#(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)
es
e'))
e'')))))\})
\mvee{} (\mneg{}(\mexists{}e':\{E| ((e' <loc e)
\mwedge{} (\muparrow{}((\mlambda{}e'.0 <z \#(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)
es
e'))
e')))\}))@i
16. (last(\mlambda{}e'.0 <z \#(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)
es
e'))
e)
= v@i
\mvdash{} sv-bag-only(lifting-2(f) (X es e)
case v
of inl(e') =>
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
e'
| inr(x) =>
init loc(e))
= (f sv-bag-only(X es e) sv-bag-only(init loc(e)))
By
Latex:
(All Reduce
THEN DVar `v'
THEN All Reduce
THEN Try (Complete (((Assert \mkleeneopen{}False\mkleeneclose{}\mcdot{} THEN Auto) THEN DVar `x' THEN RepD THEN MaAuto))))
Home
Index