Definition: bottom
`⊥ ==  fix((λx.x))`

Lemma: bottom_diverge
`¬(⊥)↓`

Definition: callbyvalue
`eval x = a in B[x] ==  PRIMITIVE`

Definition: evalall
`evalall(t) ==`
`  fix((λevalall,t. eval x = t in`
`                   if x is a pair then let a,b = x `
`                                       in eval a' = evalall a in`
`                                          eval b' = evalall b in`
`                                            <a', b'> otherwise if x is inl then eval y = evalall outl(x) in`
`                                                                                inl y`
`                                                               else if x is inr then eval y = evalall outr(x) in`
`                                                                                     inr y `
`                                                                    else x)) `
`  t`

Lemma: evalall-axiom
`evalall(Ax) ~ Ax`

Lemma: evalall-inl
`∀[x:Top]. (evalall(inl x) ~ eval y = evalall(x) in inl y)`

Lemma: evalall-inr
`∀[x:Top]. (evalall(inr x ) ~ eval y = evalall(x) in inr y )`

Lemma: evalall-pair
`∀[x,y:Top].  (evalall(<x, y>) ~ eval x' = evalall(x) in eval y' = evalall(y) in   <x', y'>)`

Definition: callbyvalueall

`let x ⟵ a in B[x] ==  eval x = evalall(a) in B[x]`

Definition: subst-exc
`subst-exc(e;t)`
`==r eval x = t in`
`    if x is lambda then λz.subst-exc(e;x z) otherwise if x is a pair then let a,b = x `
`                                                                          in eval a' = subst-exc(e;a) in`
`                                                                             eval b' = subst-exc(e;b) in`
`                                                                               <a', b'>`
`                                                      otherwise if x is inl then eval y = subst-exc(e;outl(x)) in`
`                                                                                 inl y`
`                                                                else if x is inr then eval y = subst-exc(e;outr(x)) in`
`                                                                                      inr y `
`                                                                     else x?e:v.⊥`

Lemma: unit_wf2
`Unit ∈ Type`

Lemma: sqle_wf_base
`∀[a,b:Base].  (a ≤ b ∈ ℙ)`

Lemma: istype-sqle
`∀[a,b:Base].  istype(a ≤ b)`

Definition: is-exception
`Howe's `sqle` relation is enough to define the proposition`
`(about t ∈ Base) that t is an exception.`
` `
`Note that this is not a decidable proposition! `
`If being an exception were decidable, then a program could `
`catch *all* exceptions and we would not be able`
`to use exceptions to find the modulus of continuity of functionals.`

`The test ⌜isaxiom(e?n:x.Ax) ∧b isint(e?n:x.2)⌝ can be used to distinguish between`
`canonical values that are not exceptions and exceptions *with name n*.`
`But on other exceptions e', this test will raise the exception e'`
`(as it must, for our construction of the modulus of continuity to work.)`
`⋅`

`is-exception(t) ==  exception(⊥; ⊥) ≤ t`

Lemma: is-exception_wf
`∀[t:Base]. (is-exception(t) ∈ ℙ)`

Definition: exception-with-name
`exception-with-name(n;t) ==  exception(n; ⊥) ≤ t`

Lemma: exception-with-name_wf
`∀[n:Atom2]. ∀[t:Base].  (exception-with-name(n;t) ∈ ℙ)`

Definition: exception-value
`exception-value(n;t) ==  t?n:v.v`

Lemma: exception-value_wf
`∀[n:Atom2]. ∀[t:Base].  (exception-value(n;t) ∈ Base)`

Definition: Exception
`The type of terms that are exceptions with name n and values in type T.`

`Exception(n;T) ==  {t:Base| exception-with-name(n;t) ∧ (exception-value(n;t) ∈ T)} `

Lemma: Exception_wf
`∀[n:Atom2]. ∀[T:Type].  (Exception(n;T) ∈ Type)`

Lemma: equal-in-unit
`∀[x,y:Unit].  (x = y ∈ Unit)`

Definition: has-value
`If ⌜a⌝ has a value then the call-by-value term `
`⌜eval a; 0⌝ evaluates to 0. If ⌜a⌝ diverges then so does ⌜eval a; 0⌝.`
`Thus, ⌜a⌝ has a value if and only if  ⌜0 ≤ eval a; 0⌝⋅`

`(a)↓ ==  0 ≤ eval a; 0`

Lemma: has-value_wf_base
`∀[a:Base]. ((a)↓ ∈ ℙ)`

Lemma: member-has-value
`∀[a:Base]. Ax ∈ (a)↓ supposing (a)↓`

Lemma: has-value-extensionality
`∀[a,b:Base].  (a)↓ = (b)↓ ∈ ℙ supposing (a)↓ `⇐⇒` (b)↓`

Definition: Value
`Value() ==  {x:Base| (x)↓} `

Lemma: Value_wf
`Value() ∈ Type`

Lemma: ispair-member
`∀[T:Type]. ∀[t:Base]. ∀[a,b:T].  if t is a pair then a otherwise b ∈ T supposing (t)↓`

Lemma: isinl-member
`∀[T:Type]. ∀[t:Base]. ∀[a,b:T].  if t is inl then a else b ∈ T supposing (t)↓`

Lemma: isinr-member
`∀[T:Type]. ∀[t:Base]. ∀[a,b:T].  if t is inr then a else b ∈ T supposing (t)↓`

Lemma: ispair-pair
`∀[t,x,y:Base].  t ∈ Top × Top supposing if t is a pair then inl x otherwise inr y  ~ inl x`

Lemma: not-ispair
`∀[t,a,b:Base].`
`  ∀[x,y:Top].  (if t is a pair then x otherwise y ~ y) supposing if t is a pair then inl a otherwise inr b  ~ inr b `

Lemma: ispair-bool-if-has-value
`∀[t:Base]. ispair(t) ∈ 𝔹 supposing (t)↓`

Lemma: isaxiom-bool-if-has-value
`∀[t:Base]. isaxiom(t) ∈ 𝔹 supposing (t)↓`

Lemma: isinl-bool-if-has-value
`∀[t:Base]. isinl(t) ∈ 𝔹 supposing (t)↓`

Lemma: isinr-bool-if-has-value
`∀[t:Base]. isinr(t) ∈ 𝔹 supposing (t)↓`

Lemma: islambda-bool-if-has-value
`∀[t:Base]. islambda(t) ∈ 𝔹 supposing (t)↓`

Lemma: isatom-bool-if-has-value
`∀[t:Base]. isatom(t) ∈ 𝔹 supposing (t)↓`

Lemma: isatom1-bool-if-has-value
`∀[t:Base]. isatom1(t) ∈ 𝔹 supposing (t)↓`

Lemma: isatom2-bool-if-has-value
`∀[t:Base]. isatom2(t) ∈ 𝔹 supposing (t)↓`

Lemma: isint-bool-if-has-value
`∀[t:Base]. isint(t) ∈ 𝔹 supposing (t)↓`

Lemma: decide-pair-if-has-value
`∀t:Base. ((t)↓ `` Dec(t ~ <fst(t), snd(t)>))`

Lemma: decide-axiom-if-has-value
`∀t:Base. ((t)↓ `` Dec(t ~ Ax))`

Lemma: decide-inl-if-has-value
`∀t:Base. ((t)↓ `` Dec(t ~ inl outl(t)))`

Lemma: decide-inr-if-has-value
`∀t:Base. ((t)↓ `` Dec(t ~ inr outr(t) ))`

Lemma: decide-lambda-if-has-value
`∀t:Base. ((t)↓ `` Dec(t ~ λx.(t x)))`

Lemma: decide-int-if-has-value
`∀t:Base. ((t)↓ `` Dec(t ∈ ℤ))`

Lemma: decide-atom-if-has-value
`∀t:Base. ((t)↓ `` Dec(t ∈ Atom))`

Lemma: decide-atom2-if-has-value
`∀t:Base. ((t)↓ `` Dec(t ∈ Atom2))`

Lemma: decide-ispair-if-has-value
`∀t,a,b:Base.  ((t)↓ `` ((if t is a pair then a otherwise b ~ a) ∨ (if t is a pair then a otherwise b ~ b)))`

Lemma: decide-isaxiom-if-has-value
`∀t,a,b:Base.  ((t)↓ `` ((if t = Ax then a otherwise b ~ a) ∨ (if t = Ax then a otherwise b ~ b)))`

Lemma: decide-isinl-if-has-value
`∀t,a,b:Base.  ((t)↓ `` ((if t is inl then a else b ~ a) ∨ (if t is inl then a else b ~ b)))`

Lemma: decide-isinr-if-has-value
`∀t,a,b:Base.  ((t)↓ `` ((if t is inr then a else b ~ a) ∨ (if t is inr then a else b ~ b)))`

Lemma: decide-islambda-if-has-value
`∀t,a,b:Base.  ((t)↓ `` ((if t is lambda then a otherwise b ~ a) ∨ (if t is lambda then a otherwise b ~ b)))`

Lemma: decide-isint-if-has-value
`∀t,a,b:Base.  ((t)↓ `` ((if t is an integer then a else b ~ a) ∨ (if t is an integer then a else b ~ b)))`

Lemma: decide-isatom-if-has-value
`∀t,a,b:Base.  ((t)↓ `` ((if t is an atom then a otherwise b ~ a) ∨ (if t is an atom then a otherwise b ~ b)))`

Lemma: decide-isatom2-if-has-value
`∀t,a,b:Base.  ((t)↓ `` ((isatom2(t;a;b) ~ a) ∨ (isatom2(t;a;b) ~ b)))`

Lemma: has-value-implies-dec-ispair
`∀t,a,b:Base.  ((t)↓ `` ((t ~ <fst(t), snd(t)>) ∨ (if t is a pair then a otherwise b ~ b)))`

Lemma: has-value-implies-dec-ispair-2
`∀t:Base. ((t)↓ `` ((t ~ <fst(t), snd(t)>) ∨ (∀a,b:Base.  (if t is a pair then a otherwise b ~ b))))`

Lemma: has-value-implies-dec-isaxiom
`∀t,a,b:Base.  ((t)↓ `` ((t ~ Ax) ∨ (if t = Ax then a otherwise b ~ b)))`

Lemma: has-value-implies-dec-isaxiom-2
`∀t:Base. ((t)↓ `` ((t ~ Ax) ∨ (∀a,b:Base.  (if t = Ax then a otherwise b ~ b))))`

Lemma: has-value-implies-dec-isinl
`∀t,a,b:Base.  ((t)↓ `` ((t ~ inl outl(t)) ∨ (if t is inl then a else b ~ b)))`

Lemma: has-value-implies-dec-isinl-2
`∀t:Base. ((t)↓ `` ((t ~ inl outl(t)) ∨ (∀a,b:Base.  (if t is inl then a else b ~ b))))`

Lemma: has-value-implies-dec-isinr
`∀t,a,b:Base.  ((t)↓ `` ((t ~ inr outr(t) ) ∨ (if t is inr then a else b ~ b)))`

Lemma: has-value-implies-dec-isinr-2
`∀t:Base. ((t)↓ `` ((t ~ inr outr(t) ) ∨ (∀a,b:Base.  (if t is inr then a else b ~ b))))`

Lemma: has-value-implies-dec-islambda
`∀t,a,b:Base.  ((t)↓ `` ((t ~ λx.(t x)) ∨ (if t is lambda then a otherwise b ~ b)))`

Lemma: has-value-implies-dec-islambda-2
`∀t:Base. ((t)↓ `` ((t ~ λx.(t x)) ∨ (∀a,b:Base.  (if t is lambda then a otherwise b ~ b))))`

Lemma: has-value-implies-dec-isint
`∀t,a,b:Base.  ((t)↓ `` ((t ∈ ℤ) ∨ (if t is an integer then a else b ~ b)))`

Lemma: has-value-implies-dec-isint-2
`∀t:Base. ((t)↓ `` ((t ∈ ℤ) ∨ (∀a,b:Base.  (if t is an integer then a else b ~ b))))`

Lemma: has-value-implies-dec-isatom
`∀t,a,b:Base.  ((t)↓ `` ((t ∈ Atom) ∨ (if t is an atom then a otherwise b ~ b)))`

Lemma: has-value-implies-dec-isatom-2
`∀t:Base. ((t)↓ `` ((t ∈ Atom) ∨ (∀a,b:Base.  (if t is an atom then a otherwise b ~ b))))`

Lemma: has-value-implies-dec-isatom2
`∀t,a,b:Base.  ((t)↓ `` ((t ∈ Atom2) ∨ (isatom2(t;a;b) ~ b)))`

Lemma: has-value-implies-dec-isatom2-2
`∀t:Base. ((t)↓ `` ((t ∈ Atom2) ∨ (∀a,b:Base.  (isatom2(t;a;b) ~ b))))`

Definition: is-atomic
`is-atomic(x) ==  if x is a pair then ff otherwise if x is inl then ff else if x is inr then ff else tt`

Lemma: is-atomic_wf
`∀[x:Value()]. (is-atomic(x) ∈ 𝔹)`

Definition: atomic-values
`atomic-values() ==  {x:Value()| ↑is-atomic(x)} `

Lemma: atomic-values_wf
`atomic-values() ∈ Type`

Lemma: atomic-values_subtype_base
`atomic-values() ⊆r Base`

Lemma: sq_stable__sqle
`∀[a,b:Base].  SqStable(a ≤ b)`

Definition: strict
`strict(F) ==`
`  (∀x:Base. ((F x)↓ `` (x)↓))`
`  ∧ (∀u,v:Base.  (F (exception(u; v)) ~ exception(u; v)))`
`  ∧ (∀z:Base. (is-exception(F z) `` is-exception(z)))`

Lemma: strict_wf
`∀F:Base. (strict(F) ∈ ℙ)`

Lemma: exception-not-bottom_1
`∀[nm,val:Base].  ((exception(nm; val) ≤ ⊥) `` False)`

Lemma: exception-not-axiom
`∀[nm,val:Base].  ((Ax ≤ exception(nm; val)) `` False)`

Lemma: exception-not-value_1
`∀[nm,val,t:Base].  (exception(nm; val) ≤ t) `` False supposing (t)↓`

Lemma: exception-not-value-or-bottom
`∀[nm,val,t:Base].  (exception(nm; val) ≤ t) `` False supposing ↓(t)↓ ∨ (t ~ ⊥)`

Lemma: exception-not-value2
`∀[nm,val,t:Base].  (t ≤ exception(nm; val)) `` False supposing (t)↓`

Lemma: not-exception-has-value
`∀[nm,val:Base].  ((exception(nm; val))↓ `` False)`

Lemma: exception-not-value
`∀[t:Base]. is-exception(t) `` False supposing (t)↓`

Lemma: exception-not-bottom
`is-exception(⊥) `` False`

Lemma: bottom-sqle
`∀[x:Top]. (⊥ ≤ x)`

Lemma: test_stuck_apply
`∀[x,y,z:Top].  (<x, y> z ~ ⊥)`

Lemma: cbv-reduce-strict
`∀[F,a,B:Base].`
`  F[eval x = a in`
`    B[x]] ≤ F[B[a]] `
`  supposing (∀x:Base. ((F[x])↓ `` (x)↓))`
`  ∧ (∀u,v,x:Base.  ((F[x] ~ exception(u; v)) `` (↓(x ~ exception(u; v)) ∨ (x)↓)))`
`  ∧ (∀u,v:Base.  (B[exception(u; v)] ~ exception(u; v)))`

Definition: strict1
`strict1(F) ==`
`  (∀x:Base. ((F x)↓ `` (x)↓))`
`  ∧ (∀u,v:Base.  (F (exception(u; v)) ~ exception(u; v)))`
`  ∧ (∀x:Base. (is-exception(F x) `` (↓(x)↓ ∨ is-exception(x))))`

Lemma: strict1_wf
`∀[F:Base]. (strict1(F) ∈ ℙ)`

Definition: strict2
`strict2(F) ==`
`  (∀x,y:Base.  ((F x y)↓ `` (x)↓))`
`  ∧ (∀y,u,v:Base.  (F (exception(u; v)) y ~ exception(u; v)))`
`  ∧ (∀x,y:Base.  (is-exception(F x y) `` (↓(x)↓ ∨ is-exception(x))))`

Lemma: strict2_wf
`∀[F:Base]. (strict2(F) ∈ ℙ)`

Definition: strict4
`strict4(F) ==`
`  (∀x,y,z,w:Base.  ((F x y z w)↓ `` (x)↓))`
`  ∧ (∀u,v,y,z,w:Base.  (F (exception(u; v)) y z w ~ exception(u; v)))`
`  ∧ (∀x,y,z,w:Base.  (is-exception(F x y z w) `` (↓is-exception(x) ∨ (x)↓)))`

Lemma: strict4_wf
`∀[F:Base]. (strict4(F) ∈ ℙ)`

Lemma: strict1-strict4
`∀F:Base. (strict1(F) `` strict4(λx,y,z,w. F[x]))`

Lemma: strict-strict1
`∀F:Base. (strict(F) `` strict1(λx.F[x]))`

Lemma: strict-strict4
`∀F:Base. (strict(F) `` strict4(λx,y,z,w. F[x]))`

Definition: strict5
`strict5(F) ==`
`  (∀x,y,z,w:Base.  ((F x y z w)↓ `` (x)↓))`
`  ∧ (∀u,v,y,z,w:Base.  (F (exception(u; v)) y z w ~ exception(u; v)))`
`  ∧ (∀u,v,x,y,z,w:Base.  ((F x y z w ~ exception(u; v)) `` (↓(eval y = x in y ~ exception(u; v)) ∨ (x)↓)))`

Definition: l-strict
`l-strict(F) ==`
`  ∀r:Base`
`    ((∀x:Base`
`        ((F r x)↓`
`        `` ((∀a,b:Base.  (if x is a pair then a otherwise b ~ a)) ∨ (∀a,b:Base.  (if x = Ax then a otherwise b ~ a)))))`
`    ∧ (∃G:Base. ∀x,y:Base.  ((F r <x, y> ~ G x y (r y)) ∧ strict(G x y))))`

Lemma: l-strict_wf
`∀[F:Base]. (l-strict(F) ∈ ℙ)`

Lemma: ispair-sqequal
`∀[C:Base]`
`  ∀[A,B,z:Base].`
`    if z is a pair then A z otherwise B z ~ C z `
`    supposing ((z ~ <fst(z), snd(z)>) `` (A <fst(z), snd(z)> ~ C <fst(z), snd(z)>))`
`    ∧ ((∀a,b:Base.  (if z is a pair then a otherwise b ~ b)) `` (B z ~ C z)) `
`  supposing strict(C)`

Lemma: isaxiom-sqequal
`∀[C:Base]`
`  ∀[A,B,z:Base].`
`    if z = Ax then A z otherwise B z ~ C z `
`    supposing (A Ax ~ C Ax) ∧ ((∀a,b:Base.  (if z = Ax then a otherwise b ~ b)) `` (B z ~ C z)) `
`  supposing strict(C)`

Definition: has-valueall
`has-valueall(a) ==  (evalall(a))↓`

Definition: value-type
`value-type(T) ==  ∀[x:Base]. (x)↓ supposing x ∈ T`

Lemma: value-type_wf
`∀[T:Type]. (value-type(T) ∈ Type)`

Lemma: value-type_functionality
`∀[T,T':Type].  value-type(T) `⇐⇒` value-type(T') supposing T ≡ T'`

Definition: valueall-type
`valueall-type(T) ==  ∀[x:Base]. (evalall(x))↓ supposing x ∈ T`

Lemma: valueall-type_wf
`∀[T:Type]. (valueall-type(T) ∈ Type)`

Lemma: valueall-type_functionality
`∀[T,T':Type].  valueall-type(T) `⇐⇒` valueall-type(T') supposing T ≡ T'`

Lemma: sq_stable__value-type
`∀[T:Type]. SqStable(value-type(T))`

Lemma: sq_stable__valueall-type
`∀[T:Type]. SqStable(valueall-type(T))`

Lemma: value-type-has-value
`∀[T:Type]. ∀[x:T]. (x)↓ supposing value-type(T)`

Lemma: valueall-type-has-valueall
`∀[T:Type]. ∀[x:T]. has-valueall(x) supposing valueall-type(T)`

Definition: exception-type
`exception-type(T) ==  ∀[x:Base]. is-exception(x) supposing x ∈ T`

Lemma: exception-type_wf
`∀[T:Type]. (exception-type(T) ∈ Type)`

Lemma: sq_stable_sqle
`∀[a,b:Base].  SqStable(a ≤ b)`

Lemma: sq_stable-exception-type
`∀[T:Type]. SqStable(exception-type(T))`

`∀[T:Type]. ∀[x:T]. ∀[B:Top].  let u,v = x in B[u;v] ~ x supposing exception-type(T)`

Lemma: decide-exception-type
`∀[T:Type]. ∀[x:T]. ∀[A,B:Top].  case x of inl(u) => A[u] | inr(v) => B[v] ~ x supposing exception-type(T)`

Lemma: callbyvalue-exception-type
`∀[T:Type]. ∀[x:T]. ∀[B:Top].  eval z = x in B[z] ~ x supposing exception-type(T)`

Lemma: apply-exception-type
`∀[T:Type]. ∀[x:T]. ∀[B:Top].  x B ~ x supposing exception-type(T)`

Lemma: evalall-atom
`∀[x:Atom]. (evalall(x) ~ x)`

Lemma: evalall-atom1
`∀[x:Atom1]. (evalall(x) ~ x)`

Lemma: evalall-atom2
`∀[x:Atom2]. (evalall(x) ~ x)`

Lemma: evalall-int
`∀[x:ℤ]. (evalall(x) ~ x)`

Lemma: has-value-wf-value-type
`∀[T:Type]. ∀[a:T]. ((a)↓ ∈ ℙ) supposing value-type(T)`

Lemma: sq_stable__has-value
`∀[a:Base]. SqStable((a)↓)`

Lemma: has-valueall_wf_base
`∀[a:Base]. (has-valueall(a) ∈ ℙ)`

Lemma: member-has-valueall
`∀[a:Base]. Ax ∈ has-valueall(a) supposing has-valueall(a)`

Lemma: has-valueall-has-value
`∀[a:Base]. (a)↓ supposing has-valueall(a)`

Lemma: has-valueall-if-has-value-callbyvalueall
`∀[a,b:Base].  has-valueall(a) supposing (let x ⟵ a in b[x])↓`

Lemma: sq_stable__has-valueall
`∀[a:Base]. SqStable(has-valueall(a))`

Lemma: has-valueall-pair
`∀[a,b:Base].  uiff(has-valueall(<a, b>);has-valueall(a) ∧ has-valueall(b))`

Lemma: has-valueall-inl
`∀[a:Base]. uiff(has-valueall(inl a);has-valueall(a))`

Lemma: has-valueall-inr
`∀[a:Base]. uiff(has-valueall(inr a );has-valueall(a))`

Lemma: has-valueall-lambda
`∀[a:Base]. has-valueall(λx.a[x])`

Definition: vatype
`ValueAllType ==  {T:Type| valueall-type(T)} `

Lemma: vatype_wf
`ValueAllType ∈ 𝕌'`

Lemma: subtype_rel_vatype
`ValueAllType ⊆r ValueAllType'`

Definition: map-eval
`map-eval(x.f[x];L) ==  rec-case(L) of [] => [] | a::b => r.eval a = f[a] in eval b = r in   [a / b]`

Lemma: void-value-type
`value-type(Void)`

Lemma: void-valueall-type
`valueall-type(Void)`

Lemma: product-value-type
`∀[A:Type]. ∀[B:A ⟶ Type].  value-type(a:A × B[a])`

Lemma: product-valueall-type
`∀[A:Type]. ∀[B:A ⟶ Type].  (valueall-type(A) `` (∀a:A. valueall-type(B[a])) `` valueall-type(a:A × B[a]))`

Lemma: union-value-type
`∀[A,B:Type].  value-type(A + B)`

Lemma: union-valueall-type
`∀[A,B:Type].  (valueall-type(A) `` valueall-type(B) `` valueall-type(A + B))`

Lemma: tunion-value-type
`∀[A:Type]. ∀[B:A ⟶ Type].  value-type(⋃a:A.B[a]) supposing ∀a:A. value-type(B[a])`

Lemma: tunion-valueall-type
`∀[A:Type]. ∀[B:A ⟶ Type].  valueall-type(⋃a:A.B[a]) supposing ∀a:A. valueall-type(B[a])`

Lemma: int-valueall-type
`valueall-type(ℤ)`

Lemma: int-value-type
`value-type(ℤ)`

Lemma: atom-valueall-type
`valueall-type(Atom)`

Lemma: atom-value-type
`value-type(Atom)`

Lemma: atom1-valueall-type
`valueall-type(Atom1)`

Lemma: atom1-value-type
`value-type(Atom1)`

Lemma: atom2-valueall-type
`valueall-type(Atom2)`

Lemma: atom2-value-type
`value-type(Atom2)`

Lemma: equal-valueall-type
`∀[T:Type]. ∀[x,y:T].  valueall-type(x = y ∈ T)`

Lemma: equal-value-type
`∀[T:Type]. ∀[x,y:T].  value-type(x = y ∈ T)`

Lemma: type-value-type
`value-type(Type)`

Lemma: function-valueall-type
`∀[A:Type]. ∀[B:A ⟶ Type].  valueall-type(a:A ⟶ B[a]) supposing ↓∃a:A. value-type(B[a])`

Lemma: function-value-type
`∀[A:Type]. ∀[B:A ⟶ Type].  value-type(a:A ⟶ B[a]) supposing ↓∃a:A. value-type(B[a])`

Lemma: all-value-type
`∀[A:Type]. ∀[a:A]. ∀[B:A ⟶ Type].  value-type(∀a:A. B[a]) supposing value-type(B[a])`

Lemma: function-not-int
`∀[A:Type]. ∀[B:A ⟶ Type].  ∀[f:a:A ⟶ B[a]]. (isint(f) ~ ff) supposing ↓∃a:A. value-type(B[a])`

Lemma: subtype-valueall-type
`∀[A,B:Type].  (valueall-type(A)) supposing (valueall-type(B) and (A ⊆r B))`

Lemma: subtype-value-type
`∀[A,B:Type].  (value-type(A)) supposing (value-type(B) and (A ⊆r B))`

Lemma: set-valueall-type
`∀[A:Type]. ∀[P:A ⟶ ℙ].  valueall-type({a:A| P[a]} ) supposing valueall-type(A)`

Lemma: set-value-type
`∀[A:Type]. ∀[P:A ⟶ ℙ].  value-type({a:A| P[a]} ) supposing value-type(A)`

Lemma: isect-valueall-type
`∀[A:Type]. ∀[B:A ⟶ Type].  ((∃a:A. valueall-type(B[a])) `` valueall-type(⋂a:A. B[a]))`

Lemma: isect-value-type
`∀[A:Type]. ∀[B:A ⟶ Type].  ((∃a:A. value-type(B[a])) `` value-type(⋂a:A. B[a]))`

Lemma: isaxiom-implies
`∀[t:Base]. (t ~ Ax) supposing ((↑isaxiom(t)) and (t)↓)`

Lemma: isaxiom-implies-sq
`∀[t:Base]. t ~ Ax supposing isaxiom(t) ~ tt`

Lemma: isaxiom-implies-not-isint
`∀[t:Base]. (¬↑isint(t)) supposing ((↑isaxiom(t)) and (t)↓)`

Lemma: not-axiom-member-int
`¬(Ax ∈ ℤ)`

Lemma: ispair-implies
`∀[t:Base]. (t ~ <fst(t), snd(t)>) supposing ((↑ispair(t)) and (t)↓)`

Lemma: ispair-implies-sq
`∀[t:Base]. t ~ <fst(t), snd(t)> supposing ispair(t) ~ tt`

Lemma: ispair-implies-not-isint
`∀[t:Base]. (¬↑isint(t)) supposing ((↑ispair(t)) and (t)↓)`

Lemma: not-pair-member-int
`∀[a,b:Base].  (¬(<a, b> ∈ ℤ))`

Lemma: ispair-implies-not-isatom
`∀[t:Base]. (¬↑isatom(t)) supposing ((↑ispair(t)) and (t)↓)`

Lemma: isinl-implies
`∀[t:Base]. (t ~ inl outl(t)) supposing ((↑isinl(t)) and (t)↓)`

Lemma: isinl-implies-not-isint
`∀[t:Base]. (¬↑isint(t)) supposing ((↑isinl(t)) and (t)↓)`

Lemma: isinl-implies-not-isatom
`∀[t:Base]. (¬↑isatom(t)) supposing ((↑isinl(t)) and (t)↓)`

Lemma: isinr-implies
`∀[t:Base]. (t ~ inr outr(t) ) supposing ((↑isinr(t)) and (t)↓)`

Lemma: isinr-implies-not-isint
`∀[t:Base]. (¬↑isint(t)) supposing ((↑isinr(t)) and (t)↓)`

Lemma: isinr-implies-not-isatom
`∀[t:Base]. (¬↑isatom(t)) supposing ((↑isinr(t)) and (t)↓)`

Lemma: isatom-implies-not-isint
`∀[t:Base]. (¬↑isint(t)) supposing ((↑isatom(t)) and (t)↓)`

Lemma: not-atom-member-int
`∀[t:Atom]. (¬(t ∈ ℤ))`

Lemma: isatom-implies-not-ispair
`∀[t:Base]. (¬↑ispair(t)) supposing ((↑isatom(t)) and (t)↓)`

Lemma: isint-implies-not-isatom
`∀[t:Base]. (¬↑isatom(t)) supposing ((↑isint(t)) and (t)↓)`

Lemma: atom-implies-ispair-right
`∀[b,c:Top]. ∀[a:Atom].  (if a is a pair then b otherwise c ~ c)`

Definition: any def
`We use any x for the witness of x:Void |- C  (no matter what C is).`
`The term ⌜any x⌝ must have type ⌜x:Void ⟶ C⌝, but any term has this type!`
`Therefore, we could define ⌜any x⌝ to be ⌜⊥⌝, but, because we sometimes`
`want to compute all the subterms of a extract term, it is safer to define`
`⌜any x⌝ to be a canonincal term. So we choose ⌜Ax⌝, the "simplest" canonical`
`term.⋅`

`any x ==  Ax`

Lemma: base-member-prop
`∀[T:Type]. ∀t:Base. (t ∈ T ∈ ℙ)`

Lemma: bottom-member-prop
`∀[T:Type]. (⊥ ∈ T ∈ ℙ)`

Lemma: strict4-apply
`strict4(λx,y,z,w. (x y))`

Lemma: strict4-divide
`strict4(λx,y,z,w. (x ÷ y))`

Lemma: subst-exc-basecase
`∀[v:Top]. ∀[e:Atom2].  (subst-exc(e;exception(e; v)) ~ ⊥)`

Lemma: has-value-try
`∀[t,n,B:Base].`
`  ↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)) `
`  supposing (t?n:v.B[v])↓`

Lemma: has-value-try-iff
`∀[t,n,B:Base].`
`  uiff((t?n:v.B[v])↓;↓((t)↓ ∧ (t?n:v.B[v] ~ t)) ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (t?n:v.B[v] ~ B[u]) ∧ (B[u])↓)))`

Lemma: try-is-exception
`∀[t,n,B,m,x:Base].`
`  exception(m; x) ≤ t?n:v.B[v] `
`  supposing ↓((n ∈ Atom2)`
`             ∧ (((m ∈ Atom2) ∧ (exception(m; x) ≤ t) ∧ (¬(n = m ∈ Atom2)))`
`               ∨ (∃u:Base. ((t ~ exception(n; u)) ∧ (exception(m; x) ≤ B[u])))))`
`             ∨ ((t)↓ ∧ (exception(m; x) ≤ n))`

Definition: ex-sqle
`ex-sqle(e;t;t') ==  subst-exc(e;t) ≤ subst-exc(e;t')`

Lemma: ex-sqle_wf
`∀[e:Atom2]. ∀[t,t':Base].  (ex-sqle(e;t;t') ∈ ℙ)`

Lemma: ex-sqle_transitivity
`∀[e:Atom2]. ∀[a,b,c:Base].  (ex-sqle(e;a;c)) supposing (ex-sqle(e;b;c) and ex-sqle(e;a;b))`

Lemma: ex-sqle-basecase
`∀[e:Atom2]. ∀[v,t':Base].  ex-sqle(e;exception(e; v);t')`

Home Index