Step
*
2
1
3
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. ¬↑first(e)
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. ↑e ∈b X
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(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
{ (All Reduce
THEN AllHyps i.(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)⌉ i⋅
THENA (RepUR ``State-comb rec-combined-class-opt-1`` 0 THEN Auto)
)
THEN (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\000C;f;X)⌉
0⋅
THENA (RepUR ``State-comb rec-combined-class-opt-1`` 0 THEN Auto)
)
THEN RecUnfold `es-local-pred` (-1)
THEN Reduce (-1)
THEN SplitOnHypITE (-1)
THEN Auto
THEN (SplitOnHypITE (-2) THENA MaAuto)) }
1
.....truecase.....
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. ¬↑first(e)
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. ↑e ∈b X
15. v : (∃e':{E| ((e' <loc e)
∧ (↑0 <z #(State-comb(init;f;X) es e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(State-comb(init;f;X) es e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(State-comb(init;f;X) es e')))}))@i
16. (inl pred(e))
= v
∈ ((∃e':{E| ((e' <loc e)
∧ (↑0 <z #(State-comb(init;f;X) es e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(State-comb(init;f;X) es e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(State-comb(init;f;X) es e')))})))@i
17. ¬↑first(e)
18. 0 < #(State-comb(init;f;X) es pred(e))
⊢ sv-bag-only(lifting-2(f) (X es e) case v of inl(e') => State-comb(init;f;X) es e' | inr(x) => init loc(e))
= (f sv-bag-only(X es e) sv-bag-only(State-comb(init;f;X) es pred(e)))
∈ B
2
.....falsecase.....
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. ¬↑first(e)
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. ↑e ∈b X
15. v : (∃e':{E| ((e' <loc e)
∧ (↑0 <z #(State-comb(init;f;X) es e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(State-comb(init;f;X) es e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(State-comb(init;f;X) es e')))}))@i
16. (last(λe'.0 <z #(State-comb(init;f;X) es e')) pred(e))
= v
∈ ((∃e':{E| ((e' <loc e)
∧ (↑0 <z #(State-comb(init;f;X) es e'))
∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(State-comb(init;f;X) es e'')))))})
∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(State-comb(init;f;X) es e')))})))@i
17. ¬↑first(e)
18. ¬0 < #(State-comb(init;f;X) es pred(e))
⊢ sv-bag-only(lifting-2(f) (X es e) case v of inl(e') => State-comb(init;f;X) es e' | inr(x) => init loc(e))
= (f sv-bag-only(X es 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{}((X es e) = \{\})
10. \mneg{}\muparrow{}first(e)
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. \muparrow{}e \mmember{}\msubb{} X
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(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:
(All Reduce
THEN AllHyps i.(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{} i\mcdot{}
THENA (RepUR ``State-comb rec-combined-class-opt-1`` 0 THEN Auto)
)
THEN (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)\000C
\msim{} State-comb(init;f;X)\mkleeneclose{} 0\mcdot{}
THENA (RepUR ``State-comb rec-combined-class-opt-1`` 0 THEN Auto)
)
THEN RecUnfold `es-local-pred` (-1)
THEN Reduce (-1)
THEN SplitOnHypITE (-1)
THEN Auto
THEN (SplitOnHypITE (-2) THENA MaAuto))
Home
Index