Lemma: bottom-sqequal-fix-id
⊥ ~ fix((λx.x))
Lemma: not-has-value-bottom
¬(⊥)↓
Lemma: lifting-callbyvalueall-decide-name_eq
∀[a,b,F,G,H:Top].
(let x ⟵ case name_eq(a;b) of inl(x) => F[x] | inr(x) => H[x]
in G[x] ~ case name_eq(a;b) of inl(x) => let x ⟵ F[x] in G[x] | inr(x) => let x ⟵ H[x] in G[x])
Lemma: null-strict
∀[a:Base]. (a)↓ supposing (null(a))↓
Lemma: lifting-null-spread
∀[p,F:Top]. (null(let x,y = p in F[x;y]) ~ let x,y = p in null(F[x;y]))
Lemma: concat-strict
∀[a:Base]. (a)↓ supposing (concat(a))↓
Lemma: lifting-spread-concat
∀[a,b:Top]. (concat(let x,y = a in b[x;y]) ~ let x,y = a in concat(b[x;y]))
Lemma: lifting-isaxiom-concat
∀[a,b,c:Top]. (concat(if a = Ax then b otherwise c) ~ if a = Ax then concat(b) otherwise concat(c))
Lemma: lifting-ispair-concat
∀[a,b,c:Top]. (concat(if a is a pair then b otherwise c) ~ if a is a pair then concat(b) otherwise concat(c))
Lemma: strictness-ifthenelse
∀[a,b:Top]. (if ⊥ then a else b fi ~ ⊥)
Lemma: strictness-isr
isr(⊥) ~ ⊥
Lemma: strictness-band-left
∀[a:Top]. (⊥ ∧b a ~ ⊥)
Lemma: strictness-concat
concat(⊥) ~ ⊥
Lemma: map-simple-reduce
∀[f,d,c,as:Top].
(map(f;reduce(λx,a. case d[x] of inl(u) => a | inr(v) => [c[x] / a];[];as)) ~ reduce(λx,a. case d[x]
of inl(u) =>
a
| inr(v) =>
[f c[x] / a];[];as))
Lemma: less_as_ite
∀[a,b,x,y:Top]. (if (x) < (y) then a else b ~ if x <z y then a else b fi )
Lemma: int_eq_as_ite
∀[a,b,x,y:Top]. (if x=y then a else b ~ if (x =z y) then a else b fi )
Lemma: beta_expansion
∀[F,v:Top]. (F[v] ~ (λx.F[x]) v)
Lemma: band_spread_left
∀[F,G,x:Top]. (let a,b = x in F[a;b] ∧b G ~ let a,b = x in F[a;b] ∧b G)
Lemma: append-strict-1
∀[a,b:Base]. (a)↓ supposing (a @ b)↓
Lemma: map-append-empty
∀[f,b:Top]. (map(f;b) @ [] ~ map(f;b))
Lemma: spread-append
∀[x,F,L:Top]. (let a,b = x in F[a;b] @ L ~ let a,b = x in F[a;b] @ L)
Lemma: decide-append
∀[d,F,G,L:Top]. (case d of inl(x) => F[x] | inr(y) => G[y] @ L ~ case d of inl(x) => F[x] @ L | inr(y) => G[y] @ L)
Lemma: less-append
∀[a,b,c,d,L:Top]. (if (a) < (b) then c else d @ L ~ if (a) < (b) then c @ L else (d @ L))
Lemma: append-append-nil
∀[x:Top]. ((x @ []) @ [] ~ x @ [])
Lemma: nil-append
∀[t:Top]. ([] @ t ~ t)
Lemma: spread-decide
∀[x,d,F,G:Top].
(let a,b = x
in case d[a;b] of inl(u) => F[a;b;u] | inr(u) => G[a;b;u] ~ case let a,b = x
in d[a;b]
of inl(u) =>
let a,b = x
in F[a;b;u]
| inr(u) =>
let a,b = x
in G[a;b;u])
Lemma: decide-spread
∀[p,F,G,H:Top].
(case let a,b = p in F[a;b] of inl(u) => G[u] | inr(v) => H[v] ~ let a,b = p
in case F[a;b] of inl(u) => G[u] | inr(v) => H[v])
Lemma: decide-bnot
∀[d,F,G:Top]. (case ¬bd of inl(x) => F | inr(y) => G ~ case d of inl(y) => G | inr(x) => F)
Lemma: map_reduce_spread2_to_reduce
∀[f,c,d,L:Top].
(map(f;reduce(λx,a. let y,z = x in let u,v = z in case d[y;u;v] of inl(x1) => a | inr(y1) => [c[y;u;v] / a];[];L))
~ reduce(λx,a. let y,z = x in let u,v = z in if d[y;u;v] then a else [f c[y;u;v] / a] fi ;[];L))
Lemma: apply-spread
∀[p,a,F:Top]. (let x,y = p in F[x;y] a ~ let x,y = p in F[x;y] a)
Lemma: band-simple-int_eq
∀[a,b,c:Top]. (if a=b then inl ⋅ else (inr ⋅ ) ∧b c ~ if a=b then c else (inr ⋅ ))
Lemma: band-simple-decide
∀[a,b:Top]. (case a of inl(y) => inl ⋅ | inr(z) => inr ⋅ ∧b b ~ case a of inl(y) => b | inr(z) => inr ⋅ )
Lemma: decide-simple-int_eq
∀[a,b,c,d:Top]. (case if a=b then inl ⋅ else (inr ⋅ ) of inl() => c | inr() => d ~ if a=b then c else d)
Lemma: decide-simple-less
∀[a,b,c,d:Top].
(case if (a) < (b) then inl ⋅ else (inr ⋅ ) of inl() => c | inr() => d ~ if (a) < (b) then c else d)
Lemma: lift-simple-decide-decide1
∀[X,F,G,M,N:Top].
(case case X of inl(x) => inr F[x] | inr(x) => inl G[x] of inl(a) => M[a] | inr(b) => N[b] ~ case X
of inl(x) =>
N[F[x]]
| inr(x) =>
M[G[x]])
Lemma: lift-simple-decide-decide2
∀[X,F,G,M,N:Top].
(case case X of inl(x) => inl F[x] | inr(x) => inr G[x] of inl(a) => M[a] | inr(b) => N[b] ~ case X
of inl(x) =>
M[F[x]]
| inr(x) =>
N[G[x]])
Lemma: callbyvalueall-reduce-repeat
∀[F,a:Top]. (let x ⟵ a in let y ⟵ x in F[y] ~ let x ⟵ a in F[x])
Lemma: callbyvalueall-reduce-repeat-right-branch
∀[a,d,F,G:Top].
(let x ⟵ a
in case d[x] of inl(u) => F[x;u] | inr(v) => let y ⟵ x in G[y;v] ~ let x ⟵ a
in case d[x]
of inl(u) =>
F[x;u]
| inr(v) =>
G[x;v])
Lemma: callbyvalueall-single
∀[F,a:Top]. (let x ⟵ [a] in F[x] ~ let x ⟵ a in F[[a]])
Lemma: callbyvalueall-single-append-nil
∀[F,a:Top]. (let x ⟵ [a] in let y ⟵ x @ [] in F[y] ~ let y ⟵ [a] in F[y])
Lemma: callbyvalueall-apply
∀[g:Base]. ∀[a,F:Top]. (let f ⟵ g in let x ⟵ f a in F[x] ~ let x ⟵ g a in F[x]) supposing g ~ λx.(g x)
Lemma: callbyvalueall-apply2
∀[g:Base]. ∀[a,F:Top]. let f ⟵ g in let x ⟵ f a in F[x] ~ let x ⟵ g a in F[x] supposing g ~ λx.(g x)
Lemma: callbyvalueall-single-repeat
∀[F,a:Top]. (let x ⟵ [a] in let y ⟵ x in F[y] ~ let x ⟵ [a] in F[x])
Lemma: callbyvalueall-single-sqle
∀[F,G:Base]. ∀[a:Top]. let x ⟵ a in F[x] ≤ let x ⟵ [a] in G[x] supposing ∀b:Base. (F[b] ≤ G[[b]])
Lemma: callbyvalueall-single-sqle2
∀[F,G:Base]. ∀[a:Top]. let x ⟵ [a] in G[x] ≤ let x ⟵ a in F[x] supposing ∀b:Base. (G[[b]] ≤ F[b])
Lemma: callbyvalueall-nil
∀[F:Top]. (let x ⟵ [] in F[x] ~ F[[]])
Lemma: callbyvalueall-nil2
∀[F:Top]. (let x ⟵ [] in F ~ F)
Definition: funtype
funtype(n;A;T) == primrec(n;T;λi,t. ((A (n - 1 - i)) ⟶ t))
Lemma: funtype_wf
∀[T:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type]. (funtype(n;A;T) ∈ Type)
Lemma: funtype-unroll
∀[T,A:Top]. ∀[n:ℕ]. (funtype(n;A;T) ~ if (n =z 0) then T else (A 0) ⟶ funtype(n - 1;λi.(A (i + 1));T) fi )
Lemma: funtype-unroll-last
∀[T,A:Top]. ∀[n:ℕ]. (funtype(n;A;T) ~ if (n =z 0) then T else funtype(n - 1;A;(A (n - 1)) ⟶ T) fi )
Lemma: funtype-unroll-last-eq
∀[T:Type]. ∀[n:ℕ]. ∀[A:ℕn ⟶ Type].
(funtype(n;A;T) = if (n =z 0) then T else funtype(n - 1;A;(A (n - 1)) ⟶ T) fi ∈ Type)
Lemma: funtype-split
∀[T:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. (funtype(n;A;T) = funtype(m;A;funtype(n - m;λk.(A (k + m));T)) ∈ Type)
Lemma: funtype-auto-test-case
∀m:ℕ. ∀A:ℕm ⟶ Type. ∀x:⋂x:Type. (x ⟶ x). ∀T:Type. (x ∈ funtype(0;A;T) ⟶ T)
Definition: callbyvalueall-seq
callbyvalueall-seq(L;G;F;n;m) ==
fix((λcallbyvalueall-seq,G,n. if m ≤z n then G F else let v ⟵ G (L n) in callbyvalueall-seq (λf.(G f v)) (n + 1) fi )\000C) G n
Lemma: callbyvalueall-seq_wf
∀[T:Type]. ∀[m:ℕ]. ∀[n:ℕm + 1]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:i:ℕm ⟶ funtype(i;A;A i)]. ∀[G:∀[T:Type]
(funtype(n;A;T) ⟶ T)].
∀[F:funtype(m;A;T)].
(callbyvalueall-seq(L;G;F;n;m) ∈ T)
Definition: callbyvalueall_seq
callbyvalueall_seq(L;G;F;n;m) ==
fix((λcallbyvalueall_seq,G,n. if m ≤z n then F G else let v ⟵ G (L n) in callbyvalueall_seq (λf.(G f v)) (n + 1) fi )\000C) G n
Lemma: callbyvalueall_seq_wf
∀[T,U:Type]. ∀[m:ℕ]. ∀[n:ℕm + 1]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:i:ℕm ⟶ funtype(i;A;A i)]. ∀[G:∀[T:Type]
(funtype(n;A;T) ⟶ T)].
∀[F:(funtype(m;A;T) ⟶ T) ⟶ U].
(callbyvalueall_seq(L;G;F;n;m) ∈ U)
Lemma: callbyvalueall_seq-seq
∀[L,G,F:Top]. ∀[n,m:ℕ]. (callbyvalueall-seq(L;G;F;n;m) ~ callbyvalueall_seq(L;G;λg.(g F);n;m))
Definition: cbva-seq
cbva-seq(L;F;m) == callbyvalueall-seq(L;λx.x;F;0;m)
Lemma: cbva-seq_wf
∀[T:Type]. ∀[m:ℕ]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:i:ℕm ⟶ funtype(i;A;A i)]. ∀[F:funtype(m;A;T)]. (cbva-seq(L;F;m) ∈ T)
Lemma: cbva-seq_seq
∀[L,F:Top]. ∀[m:ℕ]. (cbva-seq(L;F;m) ~ callbyvalueall_seq(L;λx.x;λf.(f F);0;m))
Definition: cbva_seq
cbva_seq(L; F; m) == callbyvalueall_seq(L;λx.x;F;0;m)
Lemma: cbva_seq_wf
∀[T,U:Type]. ∀[m:ℕ]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:i:ℕm ⟶ funtype(i;A;A i)]. ∀[F:(funtype(m;A;T) ⟶ T) ⟶ U].
(cbva_seq(L; F; m) ∈ U)
Definition: mk_lambdas-fun
mk_lambdas-fun(F;G;n;m) ==
fix((λmk_lambdas-fun,G,n. if m ≤z n then F G else λx.(mk_lambdas-fun (λf.(G f x)) (n + 1)) fi )) G n
Lemma: mk_lambdas-fun_wf
∀[T,U:Type]. ∀[m:ℕ]. ∀[n:ℕm + 1]. ∀[A:ℕm ⟶ Type]. ∀[F:(funtype(m;A;T) ⟶ T) ⟶ U].
∀[G:∀[T:Type]. (funtype(n;A;T) ⟶ T)].
(mk_lambdas-fun(F;G;n;m) ∈ funtype(m - n;λi.(A (i + n));U))
Definition: mk_lambdas_fun
mk_lambdas_fun(F;m) == mk_lambdas-fun(F;λx.x;0;m)
Lemma: mk_lambdas_fun_wf
∀[T,U:Type]. ∀[m:ℕ]. ∀[A:ℕm ⟶ Type]. ∀[F:(funtype(m;A;T) ⟶ T) ⟶ U]. (mk_lambdas_fun(F;m) ∈ funtype(m;A;U))
Definition: mk_lambdas
mk_lambdas(F;m) == primrec(m;F;λi,r,x. r)
Lemma: mk_lambdas_wf
∀[T:Type]. ∀[m:ℕ]. ∀[A:ℕm ⟶ Type]. ∀[F:T]. (mk_lambdas(F;m) ∈ funtype(m;A;T))
Lemma: mk_lambdas_unroll
∀[F:Top]. ∀[m:ℕ+]. (mk_lambdas(F;m) ~ λx.mk_lambdas(F;m - 1))
Lemma: mk_lambdas_unroll_ite
∀[F:Top]. ∀[m:ℕ]. (mk_lambdas(F;m) ~ if (m =z 0) then F else λx.mk_lambdas(F;m - 1) fi )
Lemma: mk_lambdas_unroll2
∀[F:Top]. ∀[m:ℕ+]. (mk_lambdas(F;m) ~ mk_lambdas(λx.F;m - 1))
Lemma: mk_lambdas_compose
∀[F:Top]. ∀[n,m:ℕ]. (mk_lambdas(mk_lambdas(F;n);m) ~ mk_lambdas(F;n + m))
Definition: partial_ap_gen
partial_ap_gen(g;n;s;m) == λf.(g mk_lambdas(mk_lambdas_fun(λh.mk_lambdas(h f;n - m - s);m);s))
Lemma: partial_ap_gen_wf
∀[T:Type]. ∀[n:ℕ]. ∀[s:ℕn + 1]. ∀[m:ℕ(n - s) + 1]. ∀[A:ℕn ⟶ Type]. ∀[g:funtype(n;A;T) ⟶ T].
(partial_ap_gen(g;n;s;m) ∈ funtype(m;λi.(A (s + i));T) ⟶ T)
Definition: partial_ap
partial_ap(g;n;m) == λf.(g mk_lambdas_fun(λh.mk_lambdas(h f;n - m);m))
Lemma: partial_ap_wf
∀[T:Type]. ∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[A:ℕn ⟶ Type]. ∀[g:funtype(n;A;T) ⟶ T]. (partial_ap(g;n;m) ∈ funtype(m;A;T) ⟶ T)
Definition: select_fun_ap
select_fun_ap(g;n;m) == g mk_lambdas(λx.mk_lambdas(x;n - m - 1);m)
Lemma: select_fun_ap_wf
∀[n:ℕ]. ∀[m:ℕn]. ∀[A:ℕn ⟶ Type]. ∀[g:∀[T:Type]. (funtype(n;A;T) ⟶ T)]. (select_fun_ap(g;n;m) ∈ A m)
Definition: select_fun_last
select_fun_last(g;m) == select_fun_ap(g;m + 1;m)
Lemma: select_fun_last_wf
∀[m:ℕ]. ∀[A:ℕm + 1 ⟶ Type]. ∀[g:∀[T:Type]. (funtype(m + 1;A;T) ⟶ T)]. (select_fun_last(g;m) ∈ A m)
Definition: mk_applies
mk_applies(F;G;m) == primrec(m;F;λi,r. (r (G i)))
Lemma: mk_applies_wf
∀[T:Type]. ∀[m,n:ℕ]. ∀[A:ℕm + n ⟶ Type]. ∀[G:k:ℕm ⟶ (A k)]. ∀[F:funtype(m + n;A;T)].
(mk_applies(F;G;m) ∈ funtype(n;λk.(A (m + k));T))
Lemma: mk_applies_lambdas
∀[F,G:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1]. (mk_applies(mk_lambdas(F;m);G;n) ~ mk_lambdas(F;m - n))
Lemma: mk_applies_lambdas2
∀[F,G:Top]. ∀[m:ℕ]. (mk_applies(mk_lambdas(F;m);G;m) ~ F)
Lemma: mk_applies_split
∀[F,G:Top]. ∀[n,m:ℕ]. (mk_applies(F;G;m + n) ~ mk_applies(mk_applies(F;G;m);λk.(G (m + k));n))
Lemma: mk_applies_lambdas1
∀[F,G:Top]. ∀[n:ℕ]. ∀[m:ℕn + 1]. (mk_applies(mk_lambdas(F;m);G;n) ~ mk_applies(F;λk.(G (m + k));n - m))
Lemma: mk_applies_unroll
∀[F,G:Top]. ∀[m:ℕ+]. (mk_applies(F;G;m) ~ mk_applies(F;G;m - 1) (G (m - 1)))
Lemma: mk_applies_fun
∀[F,K,v:Top]. ∀[n:ℕ]. ∀[m:ℕn + 1]. (mk_applies(F;λk.if (k =z n) then v else K k fi ;m) ~ mk_applies(F;K;m))
Lemma: mk_applies_fun2
∀[F,K,v:Top]. ∀[p,n:ℕ]. ∀[m:ℕn + 1].
(mk_applies(F;λk.if (p + k =z p + n) then v else K (p + k) fi ;m) ~ mk_applies(F;λi.(K (p + i));m))
Lemma: mk_applies_roll
∀[F,G,x:Top]. ∀[m:ℕ]. (mk_applies(F;G;m) x ~ mk_applies(F;λi.if (i =z m) then x else G i fi ;m + 1))
Lemma: mk_lambdas-fun-eta
∀[F,K:Top]. ∀[m,n:ℕ].
(mk_lambdas-fun(F;λf.mk_applies(f;K;n);n;m) ~ mk_lambdas-fun(λg.(F (λx.(g x)));λf.mk_applies(f;K;n);n;m))
Lemma: mk_lambdas_fun-eta
∀[F:Top]. ∀[m:ℕ]. (mk_lambdas_fun(F;m) ~ mk_lambdas_fun(λg.(F (λx.(g x)));m))
Lemma: mk_lambdas-fun-unroll
∀[F,K:Top]. ∀[m:ℕ+]. ∀[n:ℕm].
(mk_lambdas-fun(F;λx.mk_applies(x;K;n);n;m) ~ mk_lambdas-fun(λg,y. (F (λx.(g x y)));λx.mk_applies(x;K;n);n;m - 1))
Lemma: mk_lambdas-fun-unroll-first
∀[F,K:Top]. ∀[m:ℕ+]. ∀[n:ℕm].
(mk_lambdas-fun(F;λf.mk_applies(f;K;n);n;m) ~ λx.mk_lambdas-fun(F;λf.(mk_applies(f;K;n) x);n;m - 1))
Lemma: mk_lambdas-fun-shift-init
∀[F,K:Top]. ∀[n,m,p,q:ℕ].
(mk_lambdas-fun(F;λf.mk_applies(f;K;p + q);n;m)
~ mk_lambdas-fun(λg.(F (λf.(g mk_applies(f;K;p))));λf.mk_applies(f;λi.(K (p + i));q);n;m))
Lemma: mk_lambdas_fun-unroll
∀[F:Top]. ∀[m:ℕ+]. (mk_lambdas_fun(F;m) ~ mk_lambdas_fun(λg,y. (F (λx.(g x y)));m - 1))
Lemma: mk_lambdas_fun-unroll-first
∀[F:Top]. ∀[m:ℕ+]. (mk_lambdas_fun(F;m) ~ λx.mk_lambdas_fun(λg.(F (λf.(g (f x))));m - 1))
Lemma: mk_lambdas_fun-unroll-ite
∀[F:Top]. ∀[m:ℕ].
(mk_lambdas_fun(F;m) ~ if (m =z 0) then F (λx.x) else λx.mk_lambdas_fun(λg.(F (λf.(g (f x))));m - 1) fi )
Lemma: mk_lambdas_fun_lambdas1
∀[f:Top]. ∀[k,m:ℕ]. ∀[n:ℕm + 1].
(mk_lambdas_fun(λh.mk_lambdas(h mk_lambdas(f;n);k);m) ~ mk_lambdas(mk_lambdas_fun(λg.mk_lambdas(g f;k);m - n);n))
Lemma: mk_lambdas_fun_lambdas
∀[f:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
(mk_lambdas_fun(λh.(h mk_lambdas(f;n));m) ~ mk_lambdas(mk_lambdas_fun(λg.(g f);m - n);n))
Lemma: mk_lambdas_fun_lambdas2
∀[f:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1]. (mk_lambdas_fun(λh,x. (h mk_lambdas(f;n));m) ~ mk_lambdas(mk_lambdas_fun(λg,x. (g f);m -\000C n);n))
Lemma: mk_lambdas_fun_compose1
∀[f:Top]. ∀[k,m:ℕ]. ∀[n:ℕm + 1].
(mk_lambdas_fun(λh.mk_lambdas(h mk_lambdas_fun(f;n);k);m)
~ mk_lambdas_fun(λg.mk_lambdas_fun(λh.mk_lambdas(h (f g);k);m - n);n))
Lemma: mk_lambdas_fun_compose
∀[f:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
(mk_lambdas_fun(λh.(h mk_lambdas_fun(f;n));m) ~ mk_lambdas_fun(λg.mk_lambdas_fun(λh.(h (f g));m - n);n))
Lemma: mk_lambdas_fun_compose2
∀[f:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
(mk_lambdas_fun(λh,x. (h mk_lambdas_fun(f;n));m) ~ mk_lambdas_fun(λg.mk_lambdas_fun(λh,x. (h (f g));m - n);n))
Lemma: mk_lambdas_as_lambdas_fun
∀[F:Top]. ∀[m:ℕ]. (mk_lambdas(F;m) ~ mk_lambdas_fun(λg.F;m))
Lemma: mk_applies_lambdas_fun
∀[F,G:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
(mk_applies(mk_lambdas_fun(F;m);G;n) ~ mk_lambdas_fun(λg.(F (λx.(g mk_applies(x;G;n))));m - n))
Lemma: mk_applies_lambdas_fun0
∀[F,G:Top]. ∀[m:ℕ]. (mk_applies(mk_lambdas_fun(F;m);G;m) ~ F (λx.mk_applies(x;G;m)))
Lemma: mk_applies_lambdas_fun1
∀[F,G:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
(mk_applies(mk_lambdas_fun(F;n);G;m) ~ mk_applies(F (λx.mk_applies(x;G;n));λi.(G (n + i));m - n))
Lemma: mk_applies_ite
∀[G,b,x,y:Top]. ∀[m:ℕ].
(mk_applies(if b then x else y fi ;G;m) ~ if b then mk_applies(x;G;m) else mk_applies(y;G;m) fi )
Lemma: select_fun_ap_is_last1
∀[g:Base]. ∀[m1,m2:ℕ].
(select_fun_ap(partial_ap_gen(g;(m1 + m2) + 1;m1;m2 + 1);m2 + 1;m2) ~ select_fun_last(g;m1 + m2))
Lemma: select_fun_last_partial_ap_gen1
∀[g:Base]. ∀[m1,m2:ℕ]. (select_fun_last(partial_ap_gen(g;(m1 + m2) + 1;m1;m2 + 1);m2) ~ select_fun_last(g;m1 + m2))
Lemma: select_fun_last_partial_ap1
∀[g:Top]. ∀[m:ℕ]. (select_fun_last(partial_ap(g;m + 2;m + 1);m) ~ select_fun_ap(g;m + 2;m))
Lemma: partial_ap_of_partial_ap_gen
∀[g:Top]. ∀[m1:ℕ]. ∀[m2:ℕm1 + 1]. ∀[m3:ℕ(m1 - m2) + 1]. ∀[m4:ℕm3 + 1].
(partial_ap(partial_ap_gen(g;m1;m2;m3);m3;m4) ~ partial_ap_gen(g;m1;m2;m4))
Lemma: partial_ap_of_partial_ap_gen1
∀[g:Top]. ∀[m1,m2:ℕ].
(partial_ap(partial_ap_gen(g;(m1 + m2) + 1;m1;m2 + 1);m2 + 1;m2) ~ partial_ap_gen(g;(m1 + m2) + 1;m1;m2))
Lemma: partial_ap_is_gen
∀[g:Top]. ∀[m,n:ℕ]. (partial_ap(g;m;n) ~ partial_ap_gen(g;m;0;n))
Lemma: partial_ap_compose
∀[g:Top]. ∀[m1:ℕ]. ∀[m2:ℕm1 + 1]. ∀[m3:ℕm2 + 1]. (partial_ap(partial_ap(g;m1;m2);m2;m3) ~ partial_ap(g;m1;m3))
Definition: simple-cbva-seq
simple-cbva-seq(L;F;m) == cbva-seq(L;if (m =z 0) then F else mk_lambdas(F;m - 1) fi ;m)
Lemma: simple-cbva-seq_wf
∀[T:Type]. ∀[m:ℕ]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:i:ℕm ⟶ funtype(i;A;A i)]. ∀[F:if (m =z 0)
then T
else (A (m - 1)) ⟶ T
fi ].
(simple-cbva-seq(L;F;m) ∈ T)
Lemma: callbyvalueall-seq-fun
∀[L,K,G,F:Top]. ∀[n,m:ℕ].
(callbyvalueall-seq(λi.if i <z m then L i else K[i] fi ;G;F;n;m) ~ callbyvalueall-seq(L;G;F;n;m))
Lemma: callbyvalueall-seq-fun1
∀[L,K,G,F:Top]. ∀[n,m:ℕ]. ∀[k1,k2:ℕn + 1].
(callbyvalueall-seq(λi.if i <z k1 then L[i] else K[i] fi ;G;F;n;m) ~ callbyvalueall-seq(λi.if i <z k2
then L[i]
else K[i]
fi ;G;F;n;m))
Lemma: callbyvalueall-seq-fun2
∀[L,K,G,F:Top]. ∀[n,m:ℕ].
(callbyvalueall-seq(λi.if i <z n then L[i] else K[i] fi ;G;F;n;m) ~ callbyvalueall-seq(λi.K[i];G;F;n;m))
Lemma: callbyvalueall-seq-spread
∀[F,G,H,L,K:Top]. ∀[m:ℕ+]. ∀[n:ℕm + 1].
(let x,y = callbyvalueall-seq(L;λf.mk_applies(f;K;n);mk_lambdas(λa.<F[a], G[a]>;m - 1);n;m)
in H[x;y] ~ callbyvalueall-seq(L;λf.mk_applies(f;K;n);mk_lambdas(λa.H[F[a];G[a]];m - 1);n;m))
Lemma: callbyvalueall-seq-spread0
∀[F,G,H,L:Top]. ∀[m:ℕ+].
(let x,y = callbyvalueall-seq(L;λx.x;mk_lambdas(λa.<F[a], G[a]>;m - 1);0;m)
in H[x;y] ~ callbyvalueall-seq(L;λx.x;mk_lambdas(λa.H[F[a];G[a]];m - 1);0;m))
Lemma: simple-cbva-seq-spread
∀[F,G,H,L:Top]. ∀[m:ℕ+].
(let x,y = simple-cbva-seq(L;λa.<F[a], G[a]>;m)
in H[x;y] ~ simple-cbva-seq(L;λa.H[F[a];G[a]];m))
Lemma: simple-cbva-seq-spread0
∀[F,G,H,L:Top]. (let x,y = simple-cbva-seq(L;<F, G>;0) in H[x;y] ~ simple-cbva-seq(L;H[F;G];0))
Lemma: callbyvalueall-seq-extend
∀[F,G,L,K:Top]. ∀[m:ℕ+]. ∀[n:ℕm + 1].
(callbyvalueall-seq(L;λf.mk_applies(f;K;n);mk_lambdas(λout.let x ⟵ F[out]
in G[x];m - 1);n;m)
~ callbyvalueall-seq(λn.if (n =z m) then mk_lambdas(F;m - 1) else L n fi ;λf.mk_applies(f;K;n);mk_lambdas(G;m);n;m
+ 1))
Lemma: callbyvalueall-seq-extend-2
∀[F,G,L,K:Top]. ∀[m:ℕ+]. ∀[n:ℕm + 1].
(callbyvalueall-seq(L;λf.mk_applies(f;K;n);mk_lambdas(λout.let x ⟵ F[out]
in G[x];m - 1);n;m)
~ callbyvalueall-seq(λn.if (n =z m) then mk_lambdas(λx.F[x];m - 1) else L n fi ;λf.mk_applies(f;K;n)
;mk_lambdas(λx.G[x];m);n;m + 1))
Lemma: callbyvalueall-seq-extend0
∀[F,G,L:Top]. ∀[m:ℕ+].
(callbyvalueall-seq(L;λx.x;mk_lambdas(λout.let x ⟵ F[out]
in G[x];m - 1);0;m) ~ callbyvalueall-seq(λn.if (n =z m)
then mk_lambdas(F;m - 1)
else L n
fi ;λx.x;mk_lambdas(G;m);0;m
+ 1))
Lemma: callbyvalueall-seq-extend0-2
∀[F,G,L:Top]. ∀[m:ℕ+].
(callbyvalueall-seq(L;λx.x;mk_lambdas(λout.let x ⟵ F[out]
in G[x];m - 1);0;m) ~ callbyvalueall-seq(λn.if (n =z m)
then mk_lambdas(λx.F[x];m - 1)
else L n
fi ;λx.x;mk_lambdas(λx.G[x];m)
;0;m + 1))
Lemma: simple-cbva-seq-extend
∀[F,G,L:Top]. ∀[m:ℕ+].
(simple-cbva-seq(L;λout.let x ⟵ F[out]
in G[x];m) ~ simple-cbva-seq(λn.if (n =z m) then mk_lambdas(F;m - 1) else L n fi ;G;m + 1))
Lemma: simple-cbva-seq-extend-2
∀[F,G,L:Top]. ∀[m:ℕ+].
(simple-cbva-seq(L;λout.let x ⟵ F[out]
in G[x];m)
~ simple-cbva-seq(λn.if (n =z m) then mk_lambdas(λx.F[x];m - 1) else L n fi ;λx.G[x];m + 1))
Lemma: callbyvalueall_seq-spread
∀[F,G,H,L,K:Top]. ∀[m,n:ℕ].
(let x,y = callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.<F[g], G[g]>;n;m)
in H[x;y] ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.H[F[g];G[g]];n;m))
Lemma: callbyvalueall_seq-spread0
∀[F,G,H,L:Top]. ∀[m:ℕ].
(let x,y = callbyvalueall_seq(L;λx.x;λg.<F[g], G[g]>;0;m)
in H[x;y] ~ callbyvalueall_seq(L;λx.x;λg.H[F[g];G[g]];0;m))
Lemma: callbyvalueall_seq-decomp-last
∀[L,K,F:Top]. ∀[m:ℕ]. ∀[n:ℕm].
(callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;m) ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ g
(L (m - 1))
in F (λf.(g f x));n
;m - 1))
Lemma: callbyvalueall_seq-shift-init
∀[L,F,K:Top]. ∀[m,n,p,q:ℕ].
(callbyvalueall_seq(L;λf.mk_applies(f;K;p + q);F;n;m)
~ callbyvalueall_seq(λi.mk_applies(L i;K;p);λf.mk_applies(f;λi.(K (p + i));q);λg.(F (λf.(g mk_applies(f;K;p))));n;m))
Lemma: callbyvalueall_seq-shift-init0
∀[L,F,K:Top]. ∀[m,n,p:ℕ].
(callbyvalueall_seq(L;λf.mk_applies(f;K;p);F;n;m)
~ callbyvalueall_seq(λi.mk_applies(L i;K;p);λx.x;λg.(F (λf.(g mk_applies(f;K;p))));n;m))
Lemma: callbyvalueall_seq-shift
∀[L,F,K:Top]. ∀[m,n,k:ℕ]. (callbyvalueall_seq(λi.(L (i + k));K;F;n;m) ~ callbyvalueall_seq(L;K;F;n + k;m + k))
Lemma: callbyvalueall_seq-fun1
∀[F,G,A,B:Top]. ∀[K:ℤ ⟶ 𝔹]. ∀[n,m:ℕ].
callbyvalueall_seq(λi.if K[i] then A[i] else B[i] fi ;G;F;n;m) ~ callbyvalueall_seq(λi.B[i];G;F;n;m)
supposing ∀i:{n..m + 1-}. K[i] = ff
Lemma: callbyvalueall_seq-fun2
∀[L,K,G,F:Top]. ∀[n,m:ℕ].
(callbyvalueall_seq(λi.if i <z m then L i else K[i] fi ;G;F;n;m) ~ callbyvalueall_seq(L;G;F;n;m))
Lemma: callbyvalueall_seq-fun3
∀[L,K,G,F,J,P,Q:Top]. ∀[n,m:ℕ]. ∀[p,q:ℤ].
(callbyvalueall_seq(λi.K[if (i) < (p + q) then J[i;if i - q=p then P[i] else Q[i]] else L[i]];G;F;n;m)
~ callbyvalueall_seq(λi.K[if (i) < (p + q) then J[i;Q[i]] else L[i]];G;F;n;m))
Lemma: callbyvalueall_seq-fun4
∀[L,K,G,F,J,P,Q:Top]. ∀[n,m:ℕ]. ∀[p,q:ℤ].
(callbyvalueall_seq(λi.K[if (i) < (p + q) then J[i;λout.if i - p=q then P[i;out] else Q[i]] else L[i]];G;F;n;m)
~ callbyvalueall_seq(λi.K[if (i) < (p + q) then J[i;λout.Q[i]] else L[i]];G;F;n;m))
Lemma: callbyvalueall_seq-eta
∀[F,G,K:Top]. ∀[J:ℤ ⟶ ℤ]. ∀[n,m:ℕ].
callbyvalueall_seq(λi.(K J[i]);G;F;n;m) ~ callbyvalueall_seq(K;G;F;n;m) supposing ∀i:{n..m + 1-}. (J[i] = i ∈ ℤ)
Lemma: callbyvalueall_seq-partial-ap-all
∀[L,K,F:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
(callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;m)
~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F partial_ap(g;m;m));n;m))
Lemma: callbyvalueall_seq-partial-ap-all0
∀[L,F:Top]. ∀[m:ℕ]. (callbyvalueall_seq(L;λx.x;F;0;m) ~ callbyvalueall_seq(L;λx.x;λg.(F partial_ap(g;m;m));0;m))
Lemma: callbyvalueall_seq-lambdas-all
∀[L,G,H,K,F:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
(callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.G[f]] H[g]);n;m)
~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.(g mk_lambdas(G[f];m))] H[g]);n;m))
Lemma: callbyvalueall_seq-lambdas-all0
∀[L,G,H,F:Top]. ∀[m:ℕ].
(callbyvalueall_seq(L;λx.x;λg.(F[λf.G[f]] H[g]);0;m)
~ callbyvalueall_seq(L;λx.x;λg.(F[λf.(g mk_lambdas(G[f];m))] H[g]);0;m))
Lemma: callbyvalueall_seq-combine
∀[F,L1,L2,K:Top]. ∀[m1:ℕ+]. ∀[m2:ℕ]. ∀[n:ℕm1].
(callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.(g
mk_lambdas(λout.callbyvalueall_seq(L2[out];λx.x;λg.(g F[m2]);0;m2);m1
- 1));n;m1)
~ callbyvalueall_seq(λi.if i <z m1 then L1 i else mk_lambdas(λout.(L2[out] (i - m1));m1 - 1) fi ;λf.mk_applies(f;K;n)
;λg.(g mk_lambdas(F[m2];m1));n;m1 + m2))
Lemma: callbyvalueall_seq-combine0
∀[F,L1,L2:Top]. ∀[m1:ℕ+]. ∀[m2:ℕ].
(callbyvalueall_seq(L1;λx.x;λg.(g mk_lambdas(λout.callbyvalueall_seq(L2[out];λx.x;λg.(g F[m2]);0;m2);m1 - 1));0;m1)
~ callbyvalueall_seq(λi.if i <z m1 then L1 i else mk_lambdas(λout.(L2[out] (i - m1));m1 - 1) fi ;λx.x
;λg.(g mk_lambdas(F[m2];m1));0;m1 + m2))
Lemma: callbyvalueall_seq-combine2
∀[F,L1,L2,K:Top]. ∀[m1,m2:ℕ]. ∀[n:ℕm1 + 1].
(callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.callbyvalueall_seq(L2[g];λx.x;F;0;m2);n;m1)
~ callbyvalueall_seq(λi.if i <z m1 then L1 i else mk_lambdas_fun(λg.(L2[g] (i - m1));m1) fi ;λf.mk_applies(f;K;n)
;λg.(F partial_ap_gen(g;m1 + m2;m1;m2));n;m1 + m2))
Lemma: callbyvalueall_seq-combine2-0
∀[F,L1,L2:Top]. ∀[m1,m2:ℕ].
(callbyvalueall_seq(L1;λx.x;λg.callbyvalueall_seq(L2[g];λx.x;F;0;m2);0;m1)
~ callbyvalueall_seq(λi.if i <z m1 then L1 i else mk_lambdas_fun(λg.(L2[g] (i - m1));m1) fi ;λx.x
;λg.(F partial_ap_gen(g;m1 + m2;m1;m2));0;m1 + m2))
Lemma: callbyvalueall_seq-combine3
∀[F,L1,L2,K:Top]. ∀[m1,m2:ℕ]. ∀[n:ℕm1 + 1].
(callbyvalueall_seq(L1;λf.mk_applies(f;K;n);λg.callbyvalueall_seq(L2[g];λx.x;F[g];0;m2);n;m1)
~ callbyvalueall_seq(λi.if i <z m1 then L1 i else mk_lambdas_fun(λg.(L2[g] (i - m1));m1) fi ;λf.mk_applies(f;K;n)
;λg.(F[partial_ap(g;m1 + m2;m1)] partial_ap_gen(g;m1 + m2;m1;m2));n;m1 + m2))
Lemma: callbyvalueall_seq-combine3-0
∀[F,L1,L2:Top]. ∀[m1,m2:ℕ].
(callbyvalueall_seq(L1;λx.x;λg.callbyvalueall_seq(L2[g];λx.x;F[g];0;m2);0;m1)
~ callbyvalueall_seq(λi.if i <z m1 then L1 i else mk_lambdas_fun(λg.(L2[g] (i - m1));m1) fi ;λx.x
;λg.(F[partial_ap(g;m1 + m2;m1)] partial_ap_gen(g;m1 + m2;m1;m2));0;m1 + m2))
Lemma: callbyvalueall_seq-extend
∀[F,G,L,K:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
(callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ F[g]
in G[g;x];n;m) ~ callbyvalueall_seq(λn.if (n =z m)
then mk_lambdas_fun(λg.F[g];m)
else L n
fi ;λf.mk_applies(f;K;n)
;λg.G[partial_ap(g;m + 1;m);
select_fun_ap(g;m + 1;m)];n;m
+ 1))
Lemma: cbva_seq-spread
∀[F,G,H,L:Top]. ∀[m:ℕ]. (let x,y = cbva_seq(L; λg.<F[g], G[g]>; m) in H[x;y] ~ cbva_seq(L; λg.H[F[g];G[g]]; m))
Lemma: cbva_seq_extend
∀[F,G,L:Top]. ∀[m:ℕ].
(cbva_seq(L; λg.let x ⟵ F[g]
in G[g;x]; m) ~ cbva_seq(λn.if (n =z m) then mk_lambdas_fun(λg.F[g];m) else L n fi ;
λg.G[partial_ap(g;m + 1;m);select_fun_ap(g;m + 1;m)]; m + 1))
Lemma: cbva_seq-sqequal-n
∀L:Top. ∀F1,F2:Base. ∀m,n:ℕ. ((F1 ~n + 1 F2) ⇒ (cbva_seq(L; F1; m) ~n cbva_seq(L; F2; m)))
Lemma: cbva_seq-combine
∀[F,L1,L2:Top]. ∀[m1,m2:ℕ].
(cbva_seq(L1; λg.cbva_seq(L2[g]; F; m2); m1) ~ cbva_seq(λn.if n <z m1
then L1 n
else mk_lambdas_fun(λg.(L2[g] (n - m1));m1)
fi ; λg.(F partial_ap_gen(g;m1 + m2;m1;m2)); m1 + m2))
Lemma: cbva_seq-combine2
∀[F,L1,L2:Top]. ∀[m1,m2:ℕ].
(cbva_seq(L1; λg.cbva_seq(L2[g]; F[g]; m2); m1) ~ cbva_seq(λn.if n <z m1
then L1 n
else mk_lambdas_fun(λg.(L2[g] (n - m1));m1)
fi ; λg.(F[partial_ap(g;m1 + m2;m1)]
partial_ap_gen(g;m1 + m2;m1;m2)); m1 + m2))
Lemma: cbva_seq-list-case1
∀[F,G1,G2,L1,L2,a:Top]. ∀[m1,m2:ℕ].
(cbva_seq(λn.if (n) < (m1)
then L1 a n
else mk_lambdas_fun(λg.if n - m1=m2
then mk_lambdas_fun(λg1.((G1 g) + (G2 g1));m2)
else (L2 a (n - m1));m1); F; (m1 + m2) + 1)
~ cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.((G1 g1) + (G2 g2));m2);m1); F; (m1 + m2) + 1))
Lemma: cbva_seq-list-case2
∀[F,G,L1,L2,a:Top]. ∀[m1,m2:ℕ].
(cbva_seq(λn.if (n) < (m1)
then L1 a n
else mk_lambdas_fun(λg1.if n - m1=m2 then mk_lambdas_fun(λg2.G[g1;g2];m2) else (L2 a (n - m1));m1); F;
(m1 + m2) + 1) ~ cbva_seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas_fun(λg1.mk_lambdas_fun(λg2.G[g1;g2];m2);m1); F; (m1
+ m2)
+ 1))
Lemma: simple-cbva-seq-combine
∀[F,L1,L2:Top]. ∀[m1,m2:ℕ+].
(simple-cbva-seq(L1;λout.simple-cbva-seq(L2[out];F;m2);m1) ~ simple-cbva-seq(λn.if n <z m1
then L1 n
else mk_lambdas(λout.(L2[out]
(n - m1));m1
- 1)
fi ;F;m1 + m2))
Lemma: mk_lambdas-sqequal-n
∀[F1,F2:Base]. ∀n,m:ℕ. ((F1 ~n F2) ⇒ (mk_lambdas(F1;m) ~n + m mk_lambdas(F2;m)))
Lemma: mk_lambdas-sqequal-n2
∀[F1,F2:Base]. ∀n,m:ℕ. (((m ≤ n) ⇒ (F1 ~n - m F2)) ⇒ (mk_lambdas(F1;m) ~n mk_lambdas(F2;m)))
Lemma: simple-cbva-seq-sqequal-n
∀L:Top. ∀F1,F2:Base. ∀m,n:ℕ.
(((m ≤ (n + 2)) ⇒ (F1 ~(n - m) + 2 F2)) ⇒ (simple-cbva-seq(L;F1;m) ~n simple-cbva-seq(L;F2;m)))
Lemma: simple-cbva-seq-list
∀F:Top. ∀L1,L2:ℤ ⟶ Base. ∀m:ℕ. ((∀j:ℕm + 1. (L1 j ~ L2 j)) ⇒ (simple-cbva-seq(L1;F;m) ~ simple-cbva-seq(L2;F;m)))
Lemma: simple-cbva-seq-list-case1
∀[F,L1,L2,a:Top]. ∀[m1:ℕ+]. ∀[m2:ℕ].
(simple-cbva-seq(λn.if (n) < (m1)
then L1 a n
else mk_lambdas(λout.if n - m1=m2
then mk_lambdas(λo1.(out + o1);m2 - 1)
else (L2 a (n - m1));m1 - 1);F;(m1 + m2) + 1)
~ simple-cbva-seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas(λout1.mk_lambdas(λout2.(out1 + out2);m2 - 1);m1 - 1);F;(m1 + m2) + 1))
Lemma: simple-cbva-seq-list-case2
∀[F,L1,L2,G,a:Top]. ∀[m1:ℕ+]. ∀[m2:ℕ].
(simple-cbva-seq(λn.if (n) < (m1)
then L1 a n
else mk_lambdas(λout.if n - m1=m2
then mk_lambdas(λo1.G[out;o1];m2 - 1)
else (L2 a (n - m1));m1 - 1);F;(m1 + m2) + 1)
~ simple-cbva-seq(λn.if (n) < (m1)
then L1 a n
else if (n) < (m1 + m2)
then mk_lambdas(L2 a (n - m1);m1)
else mk_lambdas(λout1.mk_lambdas(λout2.G[out1;out2];m2 - 1);m1 - 1);F;(m1 + m2) + 1))
Definition: count_aps
count_aps(t;k) ==
fix((λcount_aps,t,k. (if t is stopped at g,f then eval k' = k + 1 in count_aps (g f) k' otherwise t.<t, k>))) t k
Definition: count_unrolls
count_unrolls(t;k) ==
fix((λcount_unrolls,t,k. (if t is stopped at g,f then
eval k' = k + 1 in
count_unrolls (g (f stop(f))) k'
otherwise t.<t, k>)))
t
k
Lemma: add-add-zero-in-top
∀[a,b:Top]. ((a + b) + 0 ~ a + b)
Lemma: decide-ifthenelse
∀[b,f1,f2,x,y:Top].
(case if b then x else y fi of inl(z) => f1[z] | inr(z) => f2[z] ~ if b
then case x of inl(z) => f1[z] | inr(z) => f2[z]
else case y of inl(z) => f1[z] | inr(z) => f2[z]
fi )
Lemma: test-bnot-nbot
∀[p:Top]. (¬b¬bp ~ p ∧b tt)
Home
Index