Lemma: lifting-strict-isaxiom
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c:Top]. (F[if a = Ax then b otherwise c;p;q;r] ~ if a = Ax then F[b;p;q;r] otherwise F[c;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-ispair
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c:Top]. (F[if a is a pair then b otherwise c;p;q;r] ~ if a is a pair then F[b;p;q;r] otherwise F[c;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-islambda
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c:Top]. (F[if a is lambda then b otherwise c;p;q;r] ~ if a is lambda then F[b;p;q;r] otherwise F[c;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-isatom
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c:Top]. (F[if a is an atom then b otherwise c;p;q;r] ~ if a is an atom then F[b;p;q;r] otherwise F[c;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-isatom2
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c:Top]. (F[isatom2(a;b;c);p;q;r] ~ isatom2(a;F[b;p;q;r];F[c;p;q;r])) supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-isint
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c:Top]. (F[if a is an integer then b else c;p;q;r] ~ if a is an integer then F[b;p;q;r] else F[c;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-less
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c,d:Top]. (F[if (a) < (b) then c else d;p;q;r] ~ if (a) < (b) then F[c;p;q;r] else F[d;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-int_eq
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c,d:Top]. (F[if a=b then c else d;p;q;r] ~ if a=b then F[c;p;q;r] else F[d;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-atom_eq
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c,d:Top]. (F[if a=b then c else d fi ;p;q;r] ~ if a=b then F[c;p;q;r] else F[d;p;q;r] fi )
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-atom_eq2
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c,d:Top]. (F[if a=2 b then c else d;p;q;r] ~ if a=2 b then F[c;p;q;r] else F[d;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-atom_eq1
∀[F:Base]. ∀[p,q,r:Top].
∀[a,b,c,d:Top]. (F[if a=1 b then c else d;p;q;r] ~ if a=1 b then F[c;p;q;r] else F[d;p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-spread
∀[F:Base]. ∀[p,q,r:Top].
∀[a,B:Top]. (F[let x,y = a in B[x;y];p;q;r] ~ let x,y = a in F[B[x;y];p;q;r]) supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-decide
∀[F:Base]. ∀[p,q,r:Top].
∀[a,A,B:Top].
(F[case a of inl(x) => A[x] | inr(x) => B[x];p;q;r] ~ case a of inl(x) => F[A[x];p;q;r] | inr(x) => F[B[x];p;q;r])
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-callbyvalue
∀[F:Base]. ∀[p,q,r:Top]. ∀[a,B:Top]. (F[eval x = a in B[x];p;q;r] ~ eval x = a in F[B[x];p;q;r]) supposing strict4(λx,\000Cy,z,w. F[x;y;z;w])
Lemma: lifting-strict-callbyvalueall
∀[F:Base]. ∀[p,q,r:Top].
∀[a,B:Top]. (F[let x ⟵ a in B[x];p;q;r] ~ let x ⟵ a in F[B[x];p;q;r]) supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: lifting-strict-ifthenelse
∀[F:Base]. ∀[p,q,r:Top].
∀[a,A,B:Top]. (F[if a then A else B fi ;p;q;r] ~ if a then F[A;p;q;r] else F[B;p;q;r] fi )
supposing strict4(λx,y,z,w. F[x;y;z;w])
Lemma: strict4-callbyvalueall
∀[C:Base]. strict4(λx,y,z,w. let x ⟵ x in C[x])
Lemma: callbyvalueall-ifthenelse
∀[C:Base]. ∀[a,A,B:Top].
(let x ⟵ if a then A else B fi
in C[x] ~ if a then let x ⟵ A in C[x] else let x ⟵ B in C[x] fi )
Lemma: lifting-spread-spread
∀[p,F,G:Top]. (let c,d = let a,b = p in F[a;b] in G[c;d] ~ let a,b = p in let c,d = F[a;b] in G[c;d])
Lemma: lifting-spread-decide
∀[a,F,G,H:Top].
(let c,d = case a of inl(x) => F[x] | inr(x) => G[x]
in H[c;d] ~ case a of inl(x) => let c,d = F[x] in H[c;d] | inr(x) => let c,d = G[x] in H[c;d])
Lemma: lifting-spread-isaxiom
∀[a,b,c,H:Top].
(let x,y = if a = Ax then b otherwise c
in H[x;y] ~ if a = Ax then let x,y = b
in H[x;y] otherwise let x,y = c
in H[x;y])
Lemma: lifting-spread-ispair
∀[a,b,c,H:Top].
(let x,y = if a is a pair then b otherwise c
in H[x;y] ~ if a is a pair then let x,y = b
in H[x;y] otherwise let x,y = c
in H[x;y])
Lemma: lifting-spread-less
∀[a,b,c,d,H:Top].
(let x,y = if (a) < (b) then c else d
in H[x;y] ~ if (a) < (b) then let x,y = c in H[x;y] else let x,y = d in H[x;y])
Lemma: lifting-spread-callbyvalue
∀[a,F,H:Top]. (let x,y = eval z = a in F[z] in H[x;y] ~ eval z = a in let x,y = F[z] in H[x;y])
Lemma: lifting-spread-callbyvalueall
∀[a,F,H:Top]. (let x,y = let z ⟵ a in F[z] in H[x;y] ~ let z ⟵ a in let x,y = F[z] in H[x;y])
Lemma: lifting-ispair-isaxiom
∀[a,b,c,d,e:Top].
(if if a = Ax then b otherwise c is a pair then d otherwise e
~ if a = Ax then if b is a pair then d otherwise e otherwise if c is a pair then d otherwise e)
Lemma: lifting-ispair-isaxiom2
∀[a,b,c,d,e:Top].
(if if a = Ax then b otherwise c is a pair then d otherwise e
~ if a = Ax then if b is a pair then d otherwise e otherwise if c is a pair then d otherwise e)
Lemma: lifting-ispair-ispair
∀[a,b,c,d,e:Top].
(if if a is a pair then b otherwise c is a pair then d otherwise e
~ if a is a pair then if b is a pair then d otherwise e otherwise if c is a pair then d otherwise e)
Lemma: lifting-ispair-less
∀[a,b,c,d,e,f:Top].
(if if (a) < (b) then c else d is a pair then e otherwise f ~ if (a) < (b)
then if c is a pair then e otherwise f
else if d is a pair then e otherwise f)
Lemma: lifting-ispair-spread
∀[a,b,c,F:Top].
(if let x,y = a
in F[x;y] is a pair then b otherwise c ~ let x,y = a
in if F[x;y] is a pair then b otherwise c)
Lemma: lifting-ispair-decide
∀[a,b,c,F,G:Top].
(if case a of inl(x) => F[x] | inr(x) => G[x] is a pair then b otherwise c ~ case a
of inl(x) =>
if F[x] is a pair then b otherwise c
| inr(x) =>
if G[x] is a pair then b otherwise c)
Lemma: lifting-isaxiom-isaxiom
∀[a,b,c,d,e:Top].
(if if a = Ax then b otherwise c = Ax then d otherwise e
~ if a = Ax then if b = Ax then d otherwise e otherwise if c = Ax then d otherwise e)
Lemma: lifting-isaxiom-ispair
∀[a,b,c,d,e:Top].
(if if a is a pair then b otherwise c = Ax then d otherwise e
~ if a is a pair then if b = Ax then d otherwise e otherwise if c = Ax then d otherwise e)
Lemma: lifting-isaxiom-less
∀[a,b,c,d,e,f:Top].
(if if (a) < (b) then c else d = Ax then e otherwise f ~ if (a) < (b)
then if c = Ax then e otherwise f
else if d = Ax then e otherwise f)
Lemma: lifting-isaxiom-spread
∀[a,b,c,F:Top]. (if let x,y = a in F[x;y] = Ax then b otherwise c ~ let x,y = a in if F[x;y] = Ax then b otherwise c)
Lemma: lifting-isaxiom-decide
∀[a,b,c,F,G:Top].
(if case a of inl(x) => F[x] | inr(x) => G[x] = Ax then b otherwise c ~ case a
of inl(x) =>
if F[x] = Ax then b otherwise c
| inr(x) =>
if G[x] = Ax then b otherwise c)
Lemma: lifting-callbyvalue-callbyvalue
∀[a,F,G:Top]. (eval x = eval y = a in F[y] in G[x] ~ eval y = a in eval x = F[y] in G[x])
Lemma: lifting-callbyvalue-decide
∀[a,F,G,H:Top].
(eval x = case a of inl(u) => F[u] | inr(v) => G[v] in
H[x] ~ case a of inl(u) => eval x = F[u] in H[x] | inr(v) => eval x = G[v] in H[x])
Lemma: lifting-callbyvalue-spread
∀[a,F,H:Top]. (eval x = let u,v = a in F[u;v] in H[x] ~ let u,v = a in eval x = F[u;v] in H[x])
Lemma: lifting-callbyvalue-int_eq
∀[a,b,c,d,H:Top]. (eval x = if a=b then c else d in H[x] ~ if a=b then eval x = c in H[x] else eval x = d in H[x])
Lemma: lifting-callbyvalue-less
∀[a,b,c,d,H:Top].
(eval x = if (a) < (b) then c else d in
H[x] ~ if (a) < (b) then eval x = c in H[x] else eval x = d in H[x])
Lemma: lifting-callbyvalue-atom_eq
∀[a,b,c,d,H:Top].
(eval x = if a=b then c else d fi in
H[x] ~ if a=b then eval x = c in H[x] else eval x = d in H[x] fi )
Lemma: lifting-callbyvalueall-int_eq
∀[a,b,c,d,H:Top]. (let x ⟵ if a=b then c else d in H[x] ~ if a=b then let x ⟵ c in H[x] else let x ⟵ d in H[x])
Lemma: lifting-callbyvalueall-ispair
∀[a,b,c,H:Top].
(let x ⟵ if a is a pair then b otherwise c
in H[x] ~ if a is a pair then let x ⟵ b
in H[x] otherwise let x ⟵ c
in H[x])
Lemma: lifting-callbyvalueall-isaxiom
∀[a,b,c,H:Top].
(let x ⟵ if a = Ax then b otherwise c
in H[x] ~ if a = Ax then let x ⟵ b
in H[x] otherwise let x ⟵ c
in H[x])
Lemma: lifting-callbyvalueall-less
∀[a,b,c,d,H:Top].
(let x ⟵ if (a) < (b) then c else d
in H[x] ~ if (a) < (b) then let x ⟵ c in H[x] else let x ⟵ d in H[x])
Lemma: lifting-callbyvalueall-atom_eq
∀[a,b,c,d,H:Top].
(let x ⟵ if a=b then c else d fi
in H[x] ~ if a=b then let x ⟵ c in H[x] else let x ⟵ d in H[x] fi )
Lemma: lifting-callbyvalueall-spread
∀[p,F,G:Top]. (let x ⟵ let a,b = p in F[a;b] in G[x] ~ let a,b = p in let x ⟵ F[a;b] in G[x])
Lemma: lifting-callbyvalueall-decide
∀[a,F,G,H:Top].
(let x ⟵ case a of inl(x) => F[x] | inr(x) => H[x]
in G[x] ~ case a of inl(x) => let x ⟵ F[x] in G[x] | inr(x) => let x ⟵ H[x] in G[x])
Lemma: lifting-decide-ispair
∀[a,b,c,F,G:Top].
(case if a is a pair then b otherwise c of inl(x) => F[x] | inr(x) => G[x] ~ if a is a pair then case b
of inl(x) =>
F[x]
| inr(x) =>
G[x] otherwise case c
of inl(x) =>
F[x]
| inr(x) =>
G[x])
Lemma: lifting-decide-isaxiom
∀[a,b,c,F,G:Top].
(case if a = Ax then b otherwise c of inl(x) => F[x] | inr(x) => G[x] ~ if a = Ax then case b
of inl(x) =>
F[x]
| inr(x) =>
G[x] otherwise case c
of inl(x) =>
F[x]
| inr(x) =>
G[x])
Lemma: lifting-decide-less
∀[a,b,c,d,F,G:Top].
(case if (a) < (b) then c else d of inl(x) => F[x] | inr(x) => G[x] ~ if (a) < (b)
then case c
of inl(x) =>
F[x]
| inr(x) =>
G[x]
else case d
of inl(x) =>
F[x]
| inr(x) =>
G[x])
Lemma: lifting-decide-callbyvalue
∀[a,H,F,G:Top].
(case eval z = a in H[z] of inl(x) => F[x] | inr(x) => G[x] ~ eval z = a in
case H[z] of inl(x) => F[x] | inr(x) => G[x])
Lemma: lifting-decide-decide
∀[a,F,G,A,B:Top].
(case case a of inl(x) => F[x] | inr(x) => G[x] of inl(x) => A[x] | inr(x) => B[x] ~ case a
of inl(x) =>
case F[x] of inl(y) => A[y] | inr(y) => B[y]
| inr(x) =>
case G[x] of inl(y) => A[y] | inr(y) => B[y])
Lemma: lifting-decide-spread
∀[a,F,A,B:Top].
(case let u,v = a in F[u;v] of inl(x) => A[x] | inr(x) => B[x] ~ let u,v = a
in case F[u;v] of inl(x) => A[x] | inr(x) => B[x])
Lemma: lifting-decide-int_eq
∀[n,m,a,b,A,B:Top].
(case if n=m then a else b of inl(x) => A[x] | inr(x) => B[x] ~ if n=m
then case a of inl(x) => A[x] | inr(x) => B[x]
else case b of inl(x) => A[x] | inr(x) => B[x])
Lemma: lifting-apply-int_eq
∀[n,m,a,b,c:Top]. (if n=m then a else b c ~ if n=m then a c else (b c))
Lemma: lifting-apply-less
∀[n,m,a,b,c:Top]. (if (n) < (m) then a else b c ~ if (n) < (m) then a c else (b c))
Lemma: lifting-apply-atom_eq
∀[n,m,a,b,c:Top]. (if n=m then a else b fi c ~ if n=m then a c else b c fi )
Lemma: lifting-apply-decide
∀[a,b,F,G:Top]. (case a of inl(x) => F[x] | inr(x) => G[x] b ~ case a of inl(x) => F[x] b | inr(x) => G[x] b)
Lemma: lifting-apply-spread
∀[a,b,B:Top]. (let x,y = a in B[x;y] b ~ let x,y = a in B[x;y] b)
Lemma: lifting-apply-ispair
∀[a,b,c,d:Top]. (if a is a pair then b otherwise c d ~ if a is a pair then b d otherwise c d)
Lemma: lifting-apply-isaxiom
∀[a,b,c,d:Top]. (if a = Ax then b otherwise c d ~ if a = Ax then b d otherwise c d)
Lemma: lifting-apply-callbyvalue
∀[a,B,c:Top]. (eval x = a in B[x] c ~ eval x = a in B[x] c)
Lemma: lifting-apply-callbyvalueall
∀[a,B,c:Top]. (let x ⟵ a in B[x] c ~ let x ⟵ a in B[x] c)
Lemma: lifting-add-spread-1
∀[a,b,C:Top]. (let x,y = b in C[x;y] + a ~ let x,y = b in C[x;y] + a)
Lemma: lifting-add-spread-2
∀[a:ℤ]. ∀[b,C:Top]. a + let x,y = b in C[x;y] ~ let x,y = b in a + C[x;y] supposing (a)↓
Lemma: lifting-add-ispair-1
∀[a,b,c,d:Top]. (if b is a pair then c otherwise d + a ~ if b is a pair then c + a otherwise d + a)
Lemma: lifting-add-ispair-2
∀[a:ℤ]. ∀[b,c,d:Top]. (a + if b is a pair then c otherwise d ~ if b is a pair then a + c otherwise a + d)
Lemma: lifting-add-isaxiom-1
∀[a,b,c,d:Top]. (if b = Ax then c otherwise d + a ~ if b = Ax then c + a otherwise d + a)
Lemma: lifting-add-isaxiom-2
∀[a:ℤ]. ∀[b,c,d:Top]. (a + if b = Ax then c otherwise d ~ if b = Ax then a + c otherwise a + d)
Lemma: normalize-decide-right
∀[a,F,G:Top]. (case a of inl(x) => F[x] | inr(x) => G[x] a ~ case a of inl(x) => F[x] | inr(x) => G[x] (inr x ))
Lemma: normalize-decide-left
∀[a,F,G:Top]. (case a of inl(x) => F[x] a | inr(x) => G[x] ~ case a of inl(x) => F[x] (inl x) | inr(x) => G[x])
Lemma: normalization-spread4
∀[p,F:Top]. (let a,b = p in F a b p ~ let a,b = p in F a b <a, b>)
Lemma: normalization-spread3
∀[p,F:Top]. (let a,b = p in F[a;b] p ~ let a,b = p in F[a;b] <a, b>)
Lemma: normalization-spread2
∀[p,F:Top]. (let a,b = p in F[a;b;p] ~ let a,b = p in F[a;b;<a, b>])
Lemma: normalization-spread
∀[p,F:Top]. (let a,b = p in F[p] ~ let a,b = p in F[<a, b>])
Lemma: normalization-isaxiom
∀[a,b,c:Top]. (if a = Ax then b a otherwise c ~ if a = Ax then b Ax otherwise c)
Lemma: strictness-callbyvalue
∀[F:Top]. (eval x = ⊥ in F[x] ~ ⊥)
Lemma: strictness-callbyvalueall
∀[F:Top]. (let x ⟵ ⊥ in F[x] ~ ⊥)
Lemma: strictness-spread
∀[F:Top]. (let a,b = ⊥ in F[a;b] ~ ⊥)
Lemma: strictness-decide
∀[F,G:Top]. (case ⊥ of inl(x) => F[x] | inr(x) => G[x] ~ ⊥)
Lemma: strictness-apply
∀[a:Top]. (⊥ a ~ ⊥)
Lemma: strictness-fix
fix(⊥) ~ ⊥
Lemma: strictness-ispair
∀[a,b:Top]. (if ⊥ is a pair then a otherwise b ~ ⊥)
Lemma: strictness-isaxiom
∀[a,b:Top]. (if ⊥ = Ax then a otherwise b ~ ⊥)
Lemma: strictness-isinl
∀[a,b:Top]. (if ⊥ is inl then a else b ~ ⊥)
Lemma: strictness-isinr
∀[a,b:Top]. (if ⊥ is inr then a else b ~ ⊥)
Lemma: strictness-islambda
∀[a,b:Top]. (if ⊥ is lambda then a otherwise b ~ ⊥)
Lemma: strictness-isatom
∀[a,b:Top]. (if ⊥ is an atom then a otherwise b ~ ⊥)
Lemma: strictness-isatom1
∀[a,b:Top]. (isatom1(⊥;a;b) ~ ⊥)
Lemma: strictness-isatom2
∀[a,b:Top]. (isatom2(⊥;a;b) ~ ⊥)
Lemma: strictness-less-left
∀[a,b,c:Top]. (if (⊥) < (a) then b else c ~ ⊥)
Lemma: strictness-less-right
∀[a,b,c:Top]. (if (a) < (⊥) then b else c ~ eval x = a in ⊥)
Lemma: strictness-int_eq-left
∀[a,b,c:Top]. (if ⊥=a then b else c ~ ⊥)
Lemma: strictness-int_eq-right
∀[a,b,c:Top]. (if a=⊥ then b else c ~ eval x = a in ⊥)
Lemma: strictness-atom_eq-left
∀[a,b,c:Top]. (if ⊥=a then b else c fi ~ ⊥)
Lemma: strictness-atom_eq-right
∀[a,b,c:Top]. (if a=⊥ then b else c fi ~ eval x = a in ⊥)
Lemma: strictness-atom1_eq-left
∀[a,b,c:Top]. (if ⊥=1 a then b else c ~ ⊥)
Lemma: strictness-atom1_eq-right
∀[a,b,c:Top]. (if a=1 ⊥ then b else c ~ eval x = a in ⊥)
Lemma: strictness-atom2_eq-left
∀[a,b,c:Top]. (if ⊥=2 a then b else c ~ ⊥)
Lemma: strictness-atom2_eq-right
∀[a,b,c:Top]. (if a=2 ⊥ then b else c ~ eval x = a in ⊥)
Lemma: strictness-add-left
∀[a:Top]. (⊥ + a ~ ⊥)
Lemma: strictness-add-right
∀[a:Top]. (a + ⊥ ~ eval x = a in ⊥)
Lemma: strictness-subtract-left
∀[a:Top]. (⊥ - a ~ ⊥)
Lemma: strictness-subtract-right
∀[a:Top]. (a - ⊥ ~ eval x = a in ⊥)
Lemma: strictness-divide-left
∀[a:Top]. (⊥ ÷ a ~ ⊥)
Lemma: strictness-divide-right
∀[a:Top]. (a ÷ ⊥ ~ eval x = a in ⊥)
Lemma: strictness-multiply-left
∀[a:Top]. (⊥ * a ~ ⊥)
Lemma: strictness-multiply-right
∀[a:Top]. (a * ⊥ ~ eval x = a in ⊥)
Lemma: strictness-remainder-left
∀[a:Top]. (⊥ rem a ~ ⊥)
Lemma: strictness-remainder-right
∀[a:Top]. (a rem ⊥ ~ eval u = a in ⊥)
Lemma: strictness-minus
-⊥ ~ ⊥
Lemma: strict4-spread
strict4(λx,y,z,w. let a,b = x in y[a;b])
Lemma: strict4-decide
strict4(λx,y,z,w. case x of inl(x) => y[x] | inr(x) => z[x])
Lemma: strict4-ispair
strict4(λx,y,z,w. if x is a pair then y otherwise z)
Lemma: stuck-spread
∀[a:Base]. ∀[F:Top]. (let x,y = a in F[x;y] ~ eval x = a in ⊥) supposing ∀b,c:Base. (if a is a pair then b otherwise c \000C~ c)
Lemma: stuck-decide
∀[a:Base]
(∀[F,H:Top]. (case a of inl(x) => F[x] | inr(x) => H[x] ~ eval x = a in ⊥)) supposing
((∀b,c:Base. (if a is inl then b else c ~ c)) and
(∀b,c:Base. (if a is inr then b else c ~ c)))
Lemma: test-lifting
∀x:Top. (if isl(x) then 1 + outl(x) else 2 fi ~ case x of inl(y) => 1 + y | inr(z) => 2)
Lemma: spread-axiom-sqequal-bottom
∀[F:Top]. (let a,b = Ax in F[a;b] ~ ⊥)
Lemma: pi1-axiom
fst(Ax) ~ ⊥
Lemma: trivial-void-arrow
∀[T,x:Top]. (x ∈ Void ⟶ T)
Lemma: decide-bottom
∀[x:Top]. (case x of inl(a) => ⊥ | inr(b) => ⊥ ~ eval u = x in ⊥)
Lemma: push-spread-into-ifthenelse
∀[a,X,Y,Z:Top].
(let c,d = a
in if X[c;d] then Y[c;d] else Z[c;d] fi ~ if let c,d = a
in X[c;d]
then let c,d = a
in Y[c;d]
else let c,d = a
in Z[c;d]
fi )
Lemma: cbv_bottom_lemma
∀X:Top. (eval x = ⊥ in X[x] ~ ⊥)
Lemma: ifthenelse_sqle
∀[a,x1,y1,x2,y2:Base].
if a then x1 else y1 fi ≤ if a then x2 else y2 fi
supposing ((∃z:Base. (a ~ inl z)) ⇒ (x1 ≤ x2)) ∧ ((∃z:Base. (a ~ inr z )) ⇒ (y1 ≤ y2))
Lemma: ifthenelse_sqequal
∀[a,x1,y1,x2,y2:Base].
if a then x1 else y1 fi ~ if a then x2 else y2 fi
supposing ((∃z:Base. (a ~ inl z)) ⇒ (x1 ~ x2)) ∧ ((∃z:Base. (a ~ inr z )) ⇒ (y1 ~ y2))
Lemma: less_sqle
∀[a,b,x1,y1,x2,y2:Base].
if (a) < (b) then x1 else y1 ≤ if (a) < (b) then x2 else y2
supposing ((a ∈ ℤ) ∧ (b ∈ ℤ)) ⇒ ((a < b ⇒ (x1 ≤ x2)) ∧ ((¬a < b) ⇒ (y1 ≤ y2)))
Lemma: less_sqequal
∀[a,b,x1,y1,x2,y2:Base].
if (a) < (b) then x1 else y1 ~ if (a) < (b) then x2 else y2
supposing ((a ∈ ℤ) ∧ (b ∈ ℤ)) ⇒ ((a < b ⇒ (x1 ~ x2)) ∧ ((¬a < b) ⇒ (y1 ~ y2)))
Lemma: cbv_sqle
∀[a,X,Y:Base]. eval x = a in X[x] ≤ eval x = a in Y[x] supposing (a)↓ ⇒ (X[a] ≤ Y[a])
Lemma: cbv_sqle_2
∀[a,b,X,Y:Base].
eval x = a in
X[x] ≤ eval x = b in
Y[x]
supposing ((a)↓ ⇒ (X[a] ≤ eval x = b in Y[x]))
∧ (∀u,v:Base. ((a ~ exception(u; v)) ⇒ (eval x = b in Y[x] ~ exception(u; v))))
Lemma: cbv_sqequal
∀[a,X,Y:Base]. eval x = a in X[x] ~ eval x = a in Y[x] supposing (a)↓ ⇒ (X[a] ~ Y[a])
Lemma: callbyvalue-then-apply
∀[f,x:Top]. (eval g = f in g x ~ f x)
Home
Index