Comment: bar_com
bar(T)⌝ was, at one time, primitive with many rules for reasoning
about it. We later realized that we could define ⌜partial(T)⌝ as a
quotient type and prove the needed lemmas about it inside Nuprl
using the rules about quotient.

This theory contains some facts that were proved about the
primitive ⌜bar(T)⌝but we have defined ⌜bar(T) partial(T) ∈ Type⌝
and reproved these facts using that definition 
(so the rules about ⌜bar(T)⌝ have been deleted.)  

Definition: bar
bar(T) ==  partial(T)

Lemma: bar_wf
[T:Type]. (bar(T) ∈ Type)

Lemma: subtype_bar
[A:Type]. A ⊆bar(A) supposing value-type(A)

Lemma: bar-base
bar(Base) ⊆Base

Lemma: bar-wf-base
[T:Type]. bar(T) ∈ Type supposing T ⊆Base

Lemma: bar_wf_base
bar(Base) ∈ Type

Lemma: has-value-wf-base
[a:Base]. ((a)↓ ∈ ℙ)

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

Lemma: subtype_bar2
[A,B:Type].  bar(A) ⊆bar(B) supposing (A ⊆B) ∧ (value-type(A) ∨ (A ⊆Base)) ∧ (value-type(B) ∨ (B ⊆Base))

Lemma: subtype_barSqtype_base
T:Type. ((T ⊆Base)  (bar(T) ⊆Base))

Lemma: add-wf-bar

[x,y:partial(Base)].  (x y ∈ bar(ℤ))

Lemma: subtract-wf-bar

[x,y:partial(Base)].  (x y ∈ bar(ℤ))

Lemma: eq_int-wf-bar

[x,y:partial(Base)].  ((x =z y) ∈ bar(𝔹))

Lemma: le_int-wf-bar

[x,y:partial(Base)].  (x ≤y ∈ bar(𝔹))

Lemma: add-wf-bar-int

[x,y:bar(ℤ)].  (x y ∈ bar(ℤ))

Lemma: subtract-wf-bar-int

[x,y:bar(ℤ)].  (x y ∈ bar(ℤ))

Lemma: eq_int-wf-bar-int

[x,y:bar(ℤ)].  ((x =z y) ∈ bar(𝔹))

Lemma: le_int-wf-bar-int

[x,y:bar(ℤ)].  (x ≤y ∈ bar(𝔹))

Lemma: add-wf-bar-nat

[x,y:bar(ℕ)].  (x y ∈ bar(ℕ))

Lemma: imax-wf-bar

[x,y:bar(ℤ)].  (imax(x;y) ∈ bar(ℤ))

Lemma: imax-wf-bar-nat

[x,y:bar(ℕ)].  (imax(x;y) ∈ bar(ℕ))

Lemma: sq_stable__has-value

[A:Type]. ∀[a:bar(A)]. SqStable((a)↓supposing value-type(A)

Lemma: member-bar-void
[x:partial(Void)]. (x ~ ⊥)

Lemma: no-value-bottom
[T:Type]. ∀[x:partial(T)]. ~ ⊥ supposing ¬(x)↓ supposing value-type(T)

Lemma: no-value-bottom-base
[x:Base]. ~ ⊥ supposing (x)↓) ∧ is-exception(x))

Lemma: not-btrue-sqeq-bottom
¬(tt ~ ⊥)

Lemma: strong-subtype-bar
[T:Type]. (value-type(T)  strong-subtype(T;bar(T)))

Lemma: equal-in-bar
[T:Type]. (value-type(T)  (∀b:bar(T). ∀a:T.  ((b a ∈ bar(T))  (b a ∈ T))))

Definition: strict-fun
StrictFun ==  partial(Void) ⟶ partial(Void)

Lemma: strict-fun_wf
StrictFun ∈ Type

Lemma: apply-strict-fun
[f:StrictFun]. (f ⊥ ~ ⊥)

Lemma: is-strict-fun
[f:Base]. f ∈ StrictFun supposing f ⊥ ~ ⊥

Lemma: apply-bottom
[t:Top]. (⊥ ~ ⊥)

Definition: lift-predicate
P? ==  λX.((X)↓  (P X))

Lemma: lift-predicate_wf
[A:Type]. ∀[P:A ⟶ ℙ].  P? ∈ bar(A) ⟶ ℙ supposing value-type(A)

Lemma: has-value-length-member-int
[l:Base]. ||l|| ∈ ℤ supposing (||l||)↓

Lemma: has-value-length-member-list
[l:Base]. l ∈ Base List supposing (||l||)↓

Lemma: bar-type-continuous
[X:ℕ ⟶ {T:Type| value-type(T)} ]. ((⋂n:ℕbar(X[n])) ⊆bar(⋂n:ℕX[n]))

Definition: aa_step_3n
aa_step_3n() ==  λf,n. if (n =z 1) then if (n rem =z 0) then (f (n ÷ 2)) else (1 (3 n)) fi 

Lemma: apply-bar
[A:Type]. ∀[B:A ⟶ Type]. ∀[f:partial(a:A ⟶ B[a])]. ∀[a:A].  a ∈ partial(B[a]) supposing value-type(B[a])

Lemma: has-value-equality-fix-bar
[T,E,S:Type].  ∀[G:T ⟶ bar(E)]. ∀[g:T ⟶ T].  ((G fix(g))↓ ∈ ℙsupposing value-type(E) ∧ (⊥ ∈ T)

Lemma: fixpoint-induction-bottom-bar
[E,S:Type].  (∀[G:S ⟶ bar(E)]. ∀[g:S ⟶ S].  (G[fix(g)] ∈ bar(E))) supposing ((⊥ ∈ S) and mono(E) and value-type(E))

Lemma: fixpoint-induction
[T:Type]. (∀f:bar(T) ⟶ bar(T). (fix(f) ∈ bar(T))) supposing (mono(T) and value-type(T))

Lemma: fix_wf_bar
[A:Type]. ∀[f:bar(A) ⟶ bar(A)]. (fix(f) ∈ bar(A)) supposing value-type(A) ∧ mono(A)

Lemma: fix_strict_diverge
f:StrictFun. (fix(f) ~ ⊥)

Lemma: no-excluded-middle
¬(∀P:ℙ(P ∨ P)))

Lemma: no-excluded-middle-squash
¬↓∀P:ℙ(P ∨ P))

Lemma: fix-of-id
fix((λx.x)) ~ ⊥

Lemma: fix-of-add
[z:Base]. (fix((λx.(x z))) ~ ⊥)

Home Index