---

Comment: bar_com
⌜bar(T)⌝ was, at one time, a 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 ⊆r bar(A) supposing value-type(A)

Lemma: bar-base
bar(Base) ⊆r Base

Lemma: bar-wf-base
∀[T:Type]. bar(T) ∈ Type supposing T ⊆r 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) ⊆r bar(B) supposing (A ⊆r B) ∧ (value-type(A) ∨ (A ⊆r Base)) ∧ (value-type(B) ∨ (B ⊆r Base))

Lemma: subtype_barSqtype_base
∀T:Type. ((T ⊆r Base) ⇒ (bar(T) ⊆r 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 ≤z 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 ≤z 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)]. x ~ ⊥ supposing ¬(x)↓ supposing value-type(T)

Lemma: no-value-bottom-base
∀[x:Base]. x ~ ⊥ 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]. (⊥ t ~ ⊥)

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])) ⊆r bar(⋂n:ℕ. X[n]))

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

Lemma: apply-bar
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:partial(a:A ⟶ B[a])]. ∀[a:A].  f 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