Step
*
1
2
1
1
1
2
of Lemma
taba-property
1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
6. u : A
7. v : A List
8. ∀ys:A List
((||v|| ≤ ||ys||)
⇒ (rec-case(v) of
[] => <init, ys>
x::xs' =>
p.let a,ys = p
in let h,t = ys
in <F[x;h;a], t>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;ys))
with starting value:
init)
, nth_tl(||v||;ys)
>
∈ (B × (A List))))
9. u1 : A
10. v1 : A List
11. (||v|| + 1) ≤ ||[u1 / v1]||
12. rec-case(v) of
[] => <init, [u1 / v1]>
x::xs' =>
p.let a,ys = p
in let h,t = ys
in <F[x;h;a], t>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;[u1 / v1]))
with starting value:
init)
, nth_tl(||v||;[u1 / v1])
>
∈ (B × (A List))
13. 0 < ||v|| + 1
⊢ let h,t = nth_tl(||v||;[u1 / v1])
in <F[u;h;accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;[u1 / v1]))
with starting value:
init)]
, t
>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v) @ [u];firstn(||v|| + 1;[u1 / v1]))
with starting value:
init)
, nth_tl((||v|| + 1) - 1;tl([u1 / v1]))
>
∈ (B × (A List))
BY
{ TACTIC:(TACTIC:TACTIC:Reduce 0 THEN Subst' (||v|| + 1) - 1 ~ ||v|| 0 THEN Auto) }
1
1. A : Type
2. B : Type
3. init : B
4. F : A ⟶ A ⟶ B ⟶ B
5. xs : A List
6. u : A
7. v : A List
8. ∀ys:A List
((||v|| ≤ ||ys||)
⇒ (rec-case(v) of
[] => <init, ys>
x::xs' =>
p.let a,ys = p
in let h,t = ys
in <F[x;h;a], t>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;ys))
with starting value:
init)
, nth_tl(||v||;ys)
>
∈ (B × (A List))))
9. u1 : A
10. v1 : A List
11. (||v|| + 1) ≤ ||[u1 / v1]||
12. rec-case(v) of
[] => <init, [u1 / v1]>
x::xs' =>
p.let a,ys = p
in let h,t = ys
in <F[x;h;a], t>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;[u1 / v1]))
with starting value:
init)
, nth_tl(||v||;[u1 / v1])
>
∈ (B × (A List))
13. 0 < ||v|| + 1
⊢ let h,t = nth_tl(||v||;[u1 / v1])
in <F[u;h;accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;[u1 / v1]))
with starting value:
init)]
, t
>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v) @ [u];firstn(||v|| + 1;[u1 / v1]))
with starting value:
init)
, nth_tl(||v||;v1)
>
∈ (B × (A List))
Latex:
Latex:
1. A : Type
2. B : Type
3. init : B
4. F : A {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B
5. xs : A List
6. u : A
7. v : A List
8. \mforall{}ys:A List
((||v|| \mleq{} ||ys||)
{}\mRightarrow{} (rec-case(v) of
[] => <init, ys>
x::xs' =>
p.let a,ys = p
in let h,t = ys
in <F[x;h;a], t>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;ys))
with starting value:
init)
, nth\_tl(||v||;ys)
>))
9. u1 : A
10. v1 : A List
11. (||v|| + 1) \mleq{} ||[u1 / v1]||
12. rec-case(v) of
[] => <init, [u1 / v1]>
x::xs' =>
p.let a,ys = p
in let h,t = ys
in <F[x;h;a], t>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;[u1 / v1]))
with starting value:
init)
, nth\_tl(||v||;[u1 / v1])
>
13. 0 < ||v|| + 1
\mvdash{} let h,t = nth\_tl(||v||;[u1 / v1])
in <F[u;h;accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v);firstn(||v||;[u1 / v1]))
with starting value:
init)]
, t
>
= <accumulate (with value a and list item p):
let x,x' = p
in F[x;x';a]
over list:
zip(rev(v) @ [u];firstn(||v|| + 1;[u1 / v1]))
with starting value:
init)
, nth\_tl((||v|| + 1) - 1;tl([u1 / v1]))
>
By
Latex:
TACTIC:(TACTIC:TACTIC:Reduce 0 THEN Subst' (||v|| + 1) - 1 \msim{} ||v|| 0 THEN Auto)
Home
Index