Comment: partial types
`Here we define the "partial" (or "bar") types first defined by`
` Constable, Smith, & Crary`

`They can be defined as quotient types.⋅`

Definition: base-partial
`base-partial(T) ==  {x:Base| x ∈ T supposing (x)↓ ∧ (¬is-exception(x))} `

Lemma: base-partial_wf
`∀[T:Type]. (base-partial(T) ∈ Type)`

Lemma: base-partial-not-exception
`∀[T:Type]. ∀[x:base-partial(T)].  (¬is-exception(x))`

Definition: per-partial
`per-partial(T;x;y) ==  uiff((x)↓;(y)↓) ∧ x = y ∈ T supposing (x)↓`

Lemma: per-partial_wf
`∀[T:Type]. ∀[x,y:Base].  (per-partial(T;x;y) ∈ ℙ)`

Lemma: per-partial-reflex
`∀[T:Type]. ∀[x:base-partial(T)].  per-partial(T;x;x)`

Lemma: per-partial-equiv_rel
`∀[T:Type]. EquivRel(base-partial(T);x,y.per-partial(T;x;y))`

Lemma: per-partial-subtype
`∀A,B:Type. ∀a,b:Base.  ((A ⊆r B) `` per-partial(A;a;b) `` per-partial(B;a;b))`

Definition: partial
`partial(T) ==  x,y:base-partial(T)//per-partial(T;x;y)`

Lemma: partial_wf
`∀[T:Type]. (partial(T) ∈ Type)`

Lemma: partial-not-exception
`∀[T:Type]. ∀[x:partial(T)].  (¬is-exception(x))`

Lemma: inclusion-partial
`∀[T:Type]. T ⊆r partial(T) supposing value-type(T)`

Lemma: inclusion-partial2
`∀[T:Type]. ∀x:T. (x ∈ partial(T)) supposing value-type(T)`

Lemma: subtype_rel_partial
`∀[A,B:Type].  partial(A) ⊆r partial(B) supposing A ⊆r B`

Lemma: base-partial-partial
`∀[A:Type]. (base-partial(partial(A)) ⊆r base-partial(A))`

Lemma: partial-partial
`∀[A:Type]. (partial(partial(A)) ⊆r partial(A))`

Lemma: partial-base
`partial(Base) ⊆r Base`

Lemma: subtype_partial_sqtype_base
`∀T:Type. ((T ⊆r Base) `` (partial(T) ⊆r Base))`

Lemma: partial_subtype_base
`∀T:Type. ((T ⊆r Base) `` (partial(T) ⊆r Base))`

Lemma: has-value_wf-partial
`∀[A:Type]. ∀[a:partial(A)]. ((a)↓ ∈ ℙ) supposing value-type(A)`

Lemma: base-equal-partial
`∀[A:Type]`
`  ∀[a,b:Base].`
`    a = b ∈ partial(A) supposing (((a)↓ `⇐⇒` (b)↓) ∧ a = b ∈ A supposing (a)↓) ∧ (¬is-exception(a)) ∧ (¬is-exception(b)) `
`  supposing value-type(A)`

Lemma: base-member-partial
`∀[A:Type]. ∀[a:Base]. (a ∈ partial(A)) supposing ((¬is-exception(a)) and a ∈ A supposing (a)↓) supposing value-type(A)`

Lemma: bottom_wf-partial
`∀[A:Type]. ⊥ ∈ partial(A) supposing value-type(A)`

Lemma: bottom_wf_function
`∀[A:Type]. ∀[B:A ⟶ Type].  ⊥ ∈ a:A ⟶ partial(B[a]) supposing ∀a:A. value-type(B[a])`

Lemma: termination-equality-base
`∀[T:Type]. ∀[x,y:Base].  x = y ∈ T supposing (x)↓ ∧ (x = y ∈ partial(T)) supposing value-type(T)`

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

Lemma: termination-equality
`∀[T:Type]. ∀[x,y:partial(T)].  x = y ∈ T supposing (x)↓ ∧ (x = y ∈ partial(T)) supposing value-type(T)`

Lemma: shorter-proof-of-termination-equality
`∀[T:Type]. ∀[x,y:partial(T)].  x = y ∈ T supposing (x)↓ ∧ (x = y ∈ partial(T)) supposing value-type(T)`

Lemma: respects-equality-partial
`∀[T:Type]. respects-equality(partial(T);T) supposing value-type(T)`

Lemma: even-shorter-proof-of-termination-equality
`∀[T:Type]. ∀[x,y:partial(T)].  x = y ∈ T supposing (x)↓ ∧ (x = y ∈ partial(T)) supposing value-type(T)`

Lemma: equal-partial
`∀[T:Type]. ∀[x,y:partial(T)].  uiff(x = y ∈ partial(T);uiff((x)↓;(y)↓) ∧ ((x)↓ `` (x = y ∈ T))) supposing value-type(T)`

Lemma: fix-not-exception
`∀[G,g:Base].  ¬is-exception(G fix(g)) supposing ∀j:ℕ. (¬is-exception(G (g^j ⊥)))`

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

Lemma: fixpoint-induction-bottom-base
`∀E,S:Type. ∀G,g:Base.`
`  ((G ∈ S ⟶ partial(E)) `` (g ∈ S ⟶ S) `` value-type(E) `` mono(E) `` (⊥ ∈ S) `` (G fix(g) ∈ partial(E)))`

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

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

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

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

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

Lemma: apply-2-partial
`∀[A,B,C:Type].`
`  (∀[f:Base]`
`     (∀[a:partial(A)]. ∀[b:partial(B)].  (f a b ∈ partial(C))) supposing `
`        ((∀a:partial(A). ∀b:partial(B).  ((f a b)↓ `` ((a)↓ ∧ (b)↓))) and `
`        (∀a:partial(A). ∀b:partial(B).  (((¬is-exception(a)) ∧ (¬is-exception(b))) `` (¬is-exception(f a b)))) and `
`        (f ∈ A ⟶ B ⟶ C))) supposing `
`     (value-type(C) and `
`     (value-type(B) ∧ (B ⊆r Base)) and `
`     (value-type(A) ∧ (A ⊆r Base)))`

`∀[x,y:partial(Base)].  (x + y ∈ partial(ℤ))`

`∀[x,y:partial(ℕ)].  (x + y ∈ partial(ℕ))`

Lemma: nat-partial-nat
`∀[n:ℕ]. (n ∈ partial(ℕ))`

Lemma: subtract-wf-partial
`∀[x,y:partial(Base)].  (x - y ∈ partial(ℤ))`

Lemma: eq_int-wf-partial
`∀[x,y:partial(Base)].  ((x =z y) ∈ partial(𝔹))`

Lemma: eq_int-wf-partial2
`∀[x,y:partial(ℤ)].  ((x =z y) ∈ partial(𝔹))`

Lemma: le_int-wf-partial
`∀[x,y:partial(Base)].  (x ≤z y ∈ partial(𝔹))`

Lemma: le_int-wf-partial2
`∀[x,y:partial(ℤ)].  (x ≤z y ∈ partial(𝔹))`

Lemma: imax-wf-partial
`∀[x,y:partial(ℤ)].  (imax(x;y) ∈ partial(ℤ))`

Lemma: bnot-wf-partial
`∀[b:partial(Base)]. (¬bb ∈ partial(𝔹))`

Lemma: band-wf-partial
`∀[a:partial(Base)]. ∀[b:partial(𝔹)].  (a ∧b b ∈ partial(𝔹))`

Lemma: no-halt-decider
`¬(∃h:partial(ℤ) ⟶ 𝔹. (h 0 = tt ∧ h ⊥ = ff))`

Lemma: ifthenelse_wf-partial-base
`∀T:Type`
`  (value-type(T) `` (∀c1,c2:partial(T). ∀b:Base.  if b then c1 else c2 fi  ∈ partial(T) supposing ¬is-exception(b)))`

Lemma: ifthenelse_wf-partial
`∀T:Type. (value-type(T) `` (∀c1,c2:partial(T). ∀b:partial(𝔹).  (if b then c1 else c2 fi  ∈ partial(T))))`

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

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

Lemma: partial-void
`∀z:partial(Void). (z ~ ⊥)`

Lemma: fix-diverges
`∀f:partial(Void) ⟶ partial(Void). (fix(f) ~ ⊥)`

Lemma: strict-fun
`∀[f:Base]. f ∈ partial(Void) ⟶ partial(Void) supposing f ⊥ ~ ⊥`

Lemma: fixpoint-induction2
`∀A:Type. ∀T:A ⟶ Type.`
`  ((A ⊆r Base)`
`  `` (∀a:A. value-type(T[a]))`
`  `` (∀a:A. mono(T[a]))`
`  `` (∀f:(a:A ⟶ partial(T[a])) ⟶ a:A ⟶ partial(T[a]) ⋂ Base. (fix(f) ∈ a:A ⟶ partial(T[a]))))`

`∀[x,y:partial(ℕ)].  {(x ∈ ℤ) ∧ (y ∈ ℤ)} supposing (x + y)↓`

`∀[x,y:partial(ℕ)].  uiff((x + y)↓;(x)↓ ∧ (y)↓)`

Lemma: no-excluded-middle-using-partial
`¬(∀P:ℙ. (P ∨ (¬P)))`

Lemma: no-excluded-middle-using-partial2
`¬(∀P:ℙ. ((↓P) ∨ (¬P)))`

Lemma: no-excluded-middle-squash-using-partial
`¬↓∀P:ℙ. (P ∨ (¬P))`

Lemma: set-axiom-of-choice-is-false
`¬Set-AC`

Lemma: strong-subtype-partial
`∀[T:Type]. (value-type(T) `` strong-subtype(T;partial(T)))`

Lemma: partial-strong-subtype-base
`∀[T:Type]. ((T ⊆r Base) `` strong-subtype(partial(T);Base))`

Definition: approx-type
`approx-type(T) ==  pertype(λ2x y.approx-per(T;x;y))`

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

Lemma: subtype-approx-type
`∀[T:Type]. T ⊆r approx-type(T) supposing mono(T) ∨ (T ⊆r Base)`

Lemma: member-approx-type
`∀[T:Type]. ∀x:Base. uiff(x ∈ approx-type(T);↓∃t:Base. ((x ≤ t) ∧ (t ∈ T)))`

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

Lemma: bottom-pair-member-approx-type
`∀[A,B:Type].  (A `` B `` (<⊥, ⊥> ∈ approx-type(A × B)))`

Home Index