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

Lemma: bottom_diverge

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

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

Lemma: evalall-axiom
evalall(Ax) Ax

Lemma: evalall-inl
[x:Top]. (evalall(inl x) eval evalall(x) in inl y)

Lemma: evalall-inr
[x:Top]. (evalall(inr eval evalall(x) in inr )

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 ⟵ in B[x] ==  eval evalall(a) in B[x]

Definition: subst-exc
==r eval in
    if is lambda then λz.subst-exc(e;x z) otherwise if is pair then let a,b 
                                                                          in eval a' subst-exc(e;a) in
                                                                             eval b' subst-exc(e;b) in
                                                                               <a', b'>
                                                      otherwise if is inl then eval subst-exc(e;outl(x)) in
                                                                                 inl y
                                                                else if is inr then eval subst-exc(e;outr(x)) in
                                                                     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 is an exception.
Note that this is not decidable proposition! 
If being an exception were decidable, then 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 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 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 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 is pair then otherwise b ∈ supposing (t)↓

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

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

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

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

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 is pair then otherwise a) ∨ (if is pair then otherwise b)))

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

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

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

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

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

Lemma: decide-isatom-if-has-value
t,a,b:Base.  ((t)↓  ((if is an atom then otherwise a) ∨ (if is an atom then otherwise 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 is pair then otherwise b)))

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

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

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

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

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

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

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

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

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

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

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

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

Lemma: has-value-implies-dec-isatom-2
t:Base. ((t)↓  ((t ∈ Atom) ∨ (∀a,b:Base.  (if is an atom then otherwise 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 is pair then ff otherwise if is inl then ff else if 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() ⊆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> ~ ⊥)

Lemma: cbv-reduce-strict
  F[eval 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 y)↓  (x)↓))
  ∧ (∀y,u,v:Base.  (F (exception(u; v)) exception(u; v)))
  ∧ (∀x,y:Base.  (is-exception(F y)  (↓(x)↓ ∨ is-exception(x))))

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

Definition: strict4
strict4(F) ==
  (∀x,y,z,w:Base.  ((F w)↓  (x)↓))
  ∧ (∀u,v,y,z,w:Base.  (F (exception(u; v)) exception(u; v)))
  ∧ (∀x,y,z,w:Base.  (is-exception(F 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 w)↓  (x)↓))
  ∧ (∀u,v,y,z,w:Base.  (F (exception(u; v)) exception(u; v)))
  ∧ (∀u,v,x,y,z,w:Base.  ((F exception(u; v))  (↓(eval in exception(u; v)) ∨ (x)↓)))

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

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

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

Lemma: isaxiom-sqequal
    if Ax then otherwise 
    supposing (A Ax Ax) ∧ ((∀a,b:Base.  (if Ax then otherwise b))  (B 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))

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

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

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

Lemma: apply-exception-type
[T:Type]. ∀[x:T]. ∀[B:Top].  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 ⟵ 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 );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 ⊆ValueAllType'

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

Lemma: void-value-type

Lemma: void-valueall-type

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

Lemma: int-value-type

Lemma: atom-valueall-type

Lemma: atom-value-type

Lemma: atom1-valueall-type

Lemma: atom1-value-type

Lemma: atom2-valueall-type

Lemma: atom2-value-type

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

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 ⊆B))

Lemma: subtype-value-type
[A,B:Type].  (value-type(A)) supposing (value-type(B) and (A ⊆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]. 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]. ~ <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 is pair then otherwise c)

Definition: any def
We use any for the witness of x:Void |- C  (no matter what 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 extract term, it is safer to define
any x⌝ to be canonincal term. So we choose ⌜Ax⌝the "simplest" canonical

any ==  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)↓ ∧ (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
  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
  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