Step
*
2
1
1
2
of Lemma
accum_split_prefix2
1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. ys : T List
7. y : T
8. ∀ZZ:(T List × A) List. ∀Z,X:T List × A.
((accum_split(g;x;f;ys) = <ZZ @ [Z], X> ∈ ((T List × A) List × T List × A))
⇒ (accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A)))
9. ZZ : (T List × A) List
10. Z : T List × A
11. X : T List × A
12. v1 : (T List × A) List
13. v3 : T List
14. v4 : A
15. [%5] : let LL,L2 = <v1, v3, v4>
in is_accum_splitting(T;A;ys;LL;L2;f;g;x)
16. accum_split(g;x;f;ys)
= <v1, v3, v4>
∈ {p:(T List × A) List × T List × A| let LL,L2 = p in is_accum_splitting(T;A;ys;LL;L2;f;g;x)}
17. ¬↑null(v1)
⊢ (if null(v3) then <v1, [y], v4>
if f <v3, v4> then <v1 @ [<v3, v4>], [y], g <v3, v4>>
else <v1, v3 @ [y], v4>
fi
= <ZZ @ [Z], X>
∈ ((T List × A) List × T List × A))
⇒ (accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A))
BY
{ xxx((InstLemma `last_lemma` [⌜T List × A⌝;⌜v1⌝]⋅ THENA Auto) THEN ExRepD)xxx }
1
1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. ys : T List
7. y : T
8. ∀ZZ:(T List × A) List. ∀Z,X:T List × A.
((accum_split(g;x;f;ys) = <ZZ @ [Z], X> ∈ ((T List × A) List × T List × A))
⇒ (accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A)))
9. ZZ : (T List × A) List
10. Z : T List × A
11. X : T List × A
12. v1 : (T List × A) List
13. v3 : T List
14. v4 : A
15. let LL,L2 = <v1, v3, v4>
in is_accum_splitting(T;A;ys;LL;L2;f;g;x)
16. accum_split(g;x;f;ys)
= <v1, v3, v4>
∈ {p:(T List × A) List × T List × A| let LL,L2 = p in is_accum_splitting(T;A;ys;LL;L2;f;g;x)}
17. ¬↑null(v1)
18. L' : (T List × A) List
19. v1 = (L' @ [last(v1)]) ∈ ((T List × A) List)
20. if null(v3) then <v1, [y], v4>
if f <v3, v4> then <v1 @ [<v3, v4>], [y], g <v3, v4>>
else <v1, v3 @ [y], v4>
fi
= <ZZ @ [Z], X>
∈ ((T List × A) List × T List × A)
⊢ accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A)
2
.....wf.....
1. A : Type
2. T : Type
3. x : A
4. g : (T List × A) ⟶ A
5. f : (T List × A) ⟶ 𝔹
6. ys : T List
7. y : T
8. ∀ZZ:(T List × A) List. ∀Z,X:T List × A.
((accum_split(g;x;f;ys) = <ZZ @ [Z], X> ∈ ((T List × A) List × T List × A))
⇒ (accum_split(g;x;f;concat(map(λp.(fst(p));ZZ @ [Z]))) = <ZZ, Z> ∈ ((T List × A) List × T List × A)))
9. ZZ : (T List × A) List
10. Z : T List × A
11. X : T List × A
12. v1 : (T List × A) List
13. v3 : T List
14. v4 : A
15. let LL,L2 = <v1, v3, v4>
in is_accum_splitting(T;A;ys;LL;L2;f;g;x)
16. accum_split(g;x;f;ys)
= <v1, v3, v4>
∈ {p:(T List × A) List × T List × A| let LL,L2 = p in is_accum_splitting(T;A;ys;LL;L2;f;g;x)}
17. ¬↑null(v1)
18. ∃L':(T List × A) List. (v1 = (L' @ [last(v1)]) ∈ ((T List × A) List))
⊢ if null(v3) then <v1, [y], v4>
if f <v3, v4> then <v1 @ [<v3, v4>], [y], g <v3, v4>>
else <v1, v3 @ [y], v4>
fi
= <ZZ @ [Z], X>
∈ ((T List × A) List × T List × A) ∈ ℙ
Latex:
Latex:
1. A : Type
2. T : Type
3. x : A
4. g : (T List \mtimes{} A) {}\mrightarrow{} A
5. f : (T List \mtimes{} A) {}\mrightarrow{} \mBbbB{}
6. ys : T List
7. y : T
8. \mforall{}ZZ:(T List \mtimes{} A) List. \mforall{}Z,X:T List \mtimes{} A.
((accum\_split(g;x;f;ys) = <ZZ @ [Z], X>)
{}\mRightarrow{} (accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));ZZ @ [Z]))) = <ZZ, Z>))
9. ZZ : (T List \mtimes{} A) List
10. Z : T List \mtimes{} A
11. X : T List \mtimes{} A
12. v1 : (T List \mtimes{} A) List
13. v3 : T List
14. v4 : A
15. [\%5] : let LL,L2 = <v1, v3, v4>
in is\_accum\_splitting(T;A;ys;LL;L2;f;g;x)
16. accum\_split(g;x;f;ys) = <v1, v3, v4>
17. \mneg{}\muparrow{}null(v1)
\mvdash{} (if null(v3) then <v1, [y], v4>
if f <v3, v4> then <v1 @ [<v3, v4>], [y], g <v3, v4>>
else <v1, v3 @ [y], v4>
fi
= <ZZ @ [Z], X>)
{}\mRightarrow{} (accum\_split(g;x;f;concat(map(\mlambda{}p.(fst(p));ZZ @ [Z]))) = <ZZ, Z>)
By
Latex:
xxx((InstLemma `last\_lemma` [\mkleeneopen{}T List \mtimes{} A\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{}]\mcdot{} THENA Auto) THEN ExRepD)xxx
Home
Index