Step
*
1
2
1
1
1
2
1
2
1
of Lemma
taba-property
.....subterm..... T:t
1:n
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
⊢ F[u;hd(nth_tl(||v||;[u1 / v1]));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)]
= 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)
∈ B
BY
{ Subst ⌜zip(rev(v) @ [u];firstn(||v|| + 1;[u1 / v1])) ~ zip(rev(v);firstn(||v||;[u1 / v1]))
@ [<u, hd(nth_tl(||v||;[u1 / v1]))>]⌝ 0⋅ }
1
.....equality.....
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
⊢ zip(rev(v) @ [u];firstn(||v|| + 1;[u1 / v1])) ~ zip(rev(v);firstn(||v||;[u1 / v1]))
@ [<u, hd(nth_tl(||v||;[u1 / v1]))>]
2
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
⊢ F[u;hd(nth_tl(||v||;[u1 / v1]));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)]
= 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])) @ [<u, hd(nth_tl(||v||;[u1 / v1]))>]
with starting value:
init)
∈ B
Latex:
Latex:
.....subterm..... T:t
1:n
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{} F[u;hd(nth\_tl(||v||;[u1 / v1]));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)]
= 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)
By
Latex:
Subst \mkleeneopen{}zip(rev(v) @ [u];firstn(||v|| + 1;[u1 / v1])) \msim{} zip(rev(v);firstn(||v||;[u1 / v1]))
@ [<u, hd(nth\_tl(||v||;[u1 / v1]))>]\mkleeneclose{} 0\mcdot{}
Home
Index