---

Lemma: decidable__equal_product
∀[A:Type]. ∀[B:A ⟶ Type].
  ((∀a,b:A.  Dec(a = b ∈ A)) ⇒ (∀a:A. ∀u,v:B[a].  Dec(u = v ∈ B[a])) ⇒ (∀x,y:a:A × B[a].  Dec(x = y ∈ (a:A × B[a]))))

Lemma: decidable__equal_nat_plus
∀x,y:ℕ+.  Dec(x = y ∈ ℕ+)

Lemma: decidable__equal_nat
∀x,y:ℕ.  Dec(x = y ∈ ℕ)

Lemma: member-decide-assert
∀[x:𝔹]. (if x then tt else inr (λx.⋅)  fi  ∈ Dec(↑x))

Definition: deq
EqDecider(T) ==  {eq:T ⟶ T ⟶ 𝔹| ∀x,y:T.  (x = y ∈ T ⇐⇒ ↑(eq x y))} 

Lemma: deq_wf
∀[T:Type]. (EqDecider(T) ∈ Type)

Lemma: deq_subtype
∀[T:Type]. (EqDecider(T) ⊆r (T ⟶ T ⟶ 𝔹))

Lemma: deq_subtype2
∀[T:Type]. (EqDecider(T) ⊆r (∀x,y:T.  Dec(x = y ∈ T)))

Lemma: deq_functionality_wrt_ext-eq
∀[A,B:Type].  EqDecider(A) ≡ EqDecider(B) supposing A ≡ B

Definition: eqof
eqof(d) ==  d

Lemma: eqof_wf
∀[T:Type]. ∀[d:EqDecider(T)].  (eqof(d) ∈ T ⟶ T ⟶ 𝔹)

Lemma: deq_property
∀[T:Type]. ∀[d:EqDecider(T)]. ∀[x,y:T].  uiff(x = y ∈ T;↑(d x y))

Lemma: deq_property2
∀[T:Type]. ∀[d:EqDecider(T)]. ∀[x,y:T].  uiff(x = y ∈ T;↑(d x y))

Lemma: deq-implies
∀[T:Type]. (EqDecider(T) ⇒ {∀x,y:T.  Dec(x = y ∈ T)})

Lemma: assert-deq
∀[T:Type]. ∀[d:EqDecider(T)]. ∀[x,y:T].  uiff(↑(d x y);x = y ∈ T)

Lemma: safe-assert-deq
∀[T:Type]. ∀[d:EqDecider(T)]. ∀[x,y:T].  uiff(↑(eqof(d) x y);x = y ∈ T)

Definition: mk_deq
mk_deq(p) ==  λx,y. isl(p x y)

Lemma: mk_deq_wf
∀[T:Type]. ∀[p:∀x,y:T.  Dec(x = y ∈ T)].  (mk_deq(p) ∈ EqDecider(T))

Lemma: mk_deq-subtype
∀[T,S:Type].  ∀[p:∀x,y:S.  Dec(x = y ∈ S)]. (mk_deq(p) ∈ EqDecider(T)) supposing strong-subtype(T;S)

Lemma: assert-pair-blex
∀[A,B:Type].
  ∀eq:EqDecider(A). ∀Ra:A ⟶ A ⟶ 𝔹. ∀Rb:B ⟶ B ⟶ 𝔹. ∀x,y:A × B.
    (↑(pair-blex(eq;Ra;Rb) x y) ⇐⇒ pair-lex(A;λa,a'. (↑(Ra a a'));λb,b'. (↑(Rb b b'))) x y)

Definition: deq-witness
deq-witness(eq) ==  λx,y. if eq x y then inl Ax else inr (λz.Ax)  fi 

Lemma: deq-witness_wf
∀[T:Type]. ∀[eq:EqDecider(T)].  (deq-witness(eq) ∈ ∀x,y:T.  Dec(x = y ∈ T))

Lemma: decidable-equal-deq
∀[T:Type]. (EqDecider(T) ⇒ (∀x,y:T.  Dec(x = y ∈ T)))

Lemma: deq-exists
∀[T:Type]. (EqDecider(T) ⇐⇒ ∀x,y:T.  Dec(x = y ∈ T))

Lemma: eqof_eq_btrue
∀[A:Type]. ∀[d:EqDecider(A)]. ∀[i:A].  (eqof(d) i i ~ tt)

Lemma: eqof_equal_btrue
∀[A:Type]. ∀[d:EqDecider(A)]. ∀[i,j:A].  eqof(d) i j ~ tt supposing i = j ∈ A

Definition: sq-decider
sq-decider(eq) ==  ∀[x,y:Base].  ((∃z:Base. (eq x y ~ inl z)) ⇒ (x ~ y))

Lemma: sq-decider_wf
∀[eq:Base]. (sq-decider(eq) ∈ ℙ)

Lemma: strong-subtype-deq
∀[A,B:Type]. ∀[d:EqDecider(B)].  d ∈ EqDecider(A) supposing strong-subtype(A;B)

Lemma: strong-subtype-deq-subtype
∀[A,B:Type].  EqDecider(B) ⊆r EqDecider(A) supposing strong-subtype(A;B)

Lemma: nat-deq-aux
∀[a,b:ℕ].  uiff(a = b ∈ ℕ;↑(a =z b))

Lemma: int-deq-aux
∀[a,b:ℤ].  uiff(a = b ∈ ℤ;↑(a =z b))

Definition: int-deq
IntDeq ==  λa,b. (a =z b)

Lemma: int-deq_wf
IntDeq ∈ EqDecider(ℤ)

Lemma: intdeq_reduce_lemma
∀y,x:Top.  (IntDeq x y ~ (x =z y))

Lemma: assert-int-deq
∀[x,y:ℤ].  uiff(↑(IntDeq x y);x = y ∈ ℤ)

Definition: nat-deq
NatDeq ==  λa,b. (a =z b)

Lemma: nat-deq_wf
NatDeq ∈ EqDecider(ℕ)

Definition: unit-deq
UnitDeq ==  λa,b. tt

Lemma: unit-deq_wf
UnitDeq ∈ EqDecider(Unit)

Lemma: atom-deq-aux
∀[a,b:Atom].  uiff(a = b ∈ Atom;↑a =a b)

Definition: atom-deq
AtomDeq ==  λa,b. a =a b

Lemma: atom-deq_wf
AtomDeq ∈ EqDecider(Atom)

Lemma: sq-decider-atom-deq
sq-decider(AtomDeq)

Lemma: atomdeq_reduce_lemma
∀y,x:Top.  (AtomDeq x y ~ x =a y)

Lemma: bool-deq-aux
∀[a,b:𝔹].  uiff(a = b;↑a =b b)

Definition: bool-deq
BoolDeq ==  λa,b. a =b b

Lemma: bool-deq_wf
BoolDeq ∈ EqDecider(𝔹)

Definition: proddeq
proddeq(a;b) ==  λp,q. ((a (fst(p)) (fst(q))) ∧b (b (snd(p)) (snd(q))))

Lemma: proddeq_wf
∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)].  (proddeq(a;b) ∈ (A × B) ⟶ (A × B) ⟶ 𝔹)

Lemma: proddeq_reduce_lemma
∀v,u,y,x,b,a:Top.  (proddeq(a;b) <x, y> <u, v> ~ (a x u) ∧b (b y v))

Definition: product-deq
product-deq(A;B;a;b) ==  proddeq(a;b)

Lemma: product-deq_wf
∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)].  (product-deq(A;B;a;b) ∈ EqDecider(A × B))

Lemma: productdeq_reduce_lemma
∀v,u,y,x,b,a,B,A:Top.  (product-deq(A;B;a;b) <x, y> <u, v> ~ (a x u) ∧b (b y v))

Lemma: assert-product-deq
∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)]. ∀[x,y:A × B].  uiff(↑(product-deq(A;B;a;b) x y);x = y ∈ (A × B))

Definition: sumdeq
sumdeq(a;b) ==
  λp,q. case p
        of inl(pa) =>
        case q of inl(qa) => a pa qa | inr(qb) => ff
        | inr(pb) =>
        case q of inl(qa) => ff | inr(qb) => b pb qb

Lemma: sumdeq_wf
∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)].  (sumdeq(a;b) ∈ (A + B) ⟶ (A + B) ⟶ 𝔹)

Lemma: subtype-deq
∀[A,B:Type].  (EqDecider(B) ⊆r EqDecider(A)) supposing ((∀x,y:A.  ((x = y ∈ B) ⇒ (x = y ∈ A))) and (A ⊆r B))

Lemma: subtype_rel-deq
∀[A,B:Type].  (EqDecider(B) ⊆r EqDecider(A)) supposing ((∀x,y:A.  ((x = y ∈ B) ⇒ (x = y ∈ A))) and (A ⊆r B))

Definition: union-deq
union-deq(A;B;a;b) ==  sumdeq(a;b)

Lemma: union-deq_wf
∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)].  (union-deq(A;B;a;b) ∈ EqDecider(A + B))

Lemma: assert-union-deq
∀[A,B:Type]. ∀[a:EqDecider(A)]. ∀[b:EqDecider(B)]. ∀[x,y:A + B].  uiff(↑(union-deq(A;B;a;b) x y);x = y ∈ (A + B))

Definition: finite-fun-deq
finite-fun-deq(k;eq) ==  λf,g. bdd-all(k;i.eq (f i) (g i))

Lemma: finite-fun-deq_wf
∀[T:Type]. ∀[k:ℕ]. ∀[eq:EqDecider(T)].  (finite-fun-deq(k;eq) ∈ EqDecider(ℕk ⟶ T))

Lemma: assert-finite-fun-deq
∀[T:Type]. ∀[k:ℕ]. ∀[eq:EqDecider(T)]. ∀[f,g:ℕk ⟶ T].  uiff(↑(finite-fun-deq(k;eq) f g);f = g ∈ (ℕk ⟶ T))



Home Index