Comment: rel_1_summary
Common properties of binary relations.

Comment: rel_1_intro
Common properties of binary relations are defined,
and various basic facts about them are proven.

Binary relations are treated here as terms with arguments
supplied as subterms. See binrel_com for more information
on the pros and cons of this. See the gen_algebra_1 theory
for an alternate treatment. 

Comment: binrel_com

There is design choice here with choosing whether to build theories
of relations using first-order or higher-order syntax. For example, we
could write:

A)     Refl(T;R) == ∀x:T. (R x)             (higher order)


B)     Refl(T;x,y.R[x;y]) == ∀x:T. R[x; x]   (first order)

The approaches are equivalent.

The pros for A) are:
1. Consise definitions, no extra binding vars floating around.
   (Esp with things like symmetrize).
2. Treating relations as first class objects.

The pros for B) are:
1. Most binary relations are defined using 1st order syntax
   (subterm slots for args rather than args supplied using application)
   This gives much more flexibility with relation display forms.

2. Functionality lemmas can easily be proven that allow rewriting of 
   wrt <=>With A) functionality lemmas are required for instances of
   of typed lambda terms and one would have to introduce special rw relations for
   equivalence of binary relations. (The rewrite package doesn't currently
   handle general higher order equivalence relations. (Relations on objects in 
   function types where the relations on domain and range types are arbitrary
   equivalence relations.)

3. Abstraction expansion does appropriate substitutions when we have concrete
   instances of R.

For now, go with approach B), though approach A) is think ultimately more


Definition: refl
(basic):: Refl(T;x,y.E[x; y]) ==  ∀a:T. E[a; a]

Definition: urefl
(basic):: UniformlyRefl(T;x,y.E[x; y]) ==  ∀[a:T]. E[a; a]

Lemma: refl_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (Refl(T;x,y.E[x;y]) ∈ ℙ)

Lemma: urefl_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (UniformlyRefl(T;x,y.E[x;y]) ∈ ℙ)

Lemma: refl_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R[x;y] ⇐⇒ R'[x;y]))  (Refl(T;x,y.R[x;y]) ⇐⇒ Refl(T;x,y.R'[x;y])))

Lemma: urefl_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  (R[x;y] ⇐⇒ R'[x;y]))  (UniformlyRefl(T;x,y.R[x;y]) ⇐⇒ UniformlyRefl(T;x,y.R'[x;y])))

Definition: sym
(basic):: Sym(T;x,y.E[x; y]) ==  ∀a,b:T.  (E[a; b]  E[b; a])

Definition: usym
(basic):: UniformlySym(T;x,y.E[x; y]) ==  ∀[a,b:T].  (E[a; b]  E[b; a])

Lemma: sym_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (Sym(T;x,y.E[x;y]) ∈ ℙ)

Lemma: usym_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (UniformlySym(T;x,y.E[x;y]) ∈ ℙ)

Lemma: sym_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R[x;y] ⇐⇒ R'[x;y]))  (Sym(T;x,y.R[x;y]) ⇐⇒ Sym(T;x,y.R'[x;y])))

Lemma: usym_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  (R[x;y] ⇐⇒ R'[x;y]))  (UniformlySym(T;x,y.R[x;y]) ⇐⇒ UniformlySym(T;x,y.R'[x;y])))

Definition: trans
(basic):: Trans(T;x,y.E[x; y]) ==  ∀a,b,c:T.  (E[a; b]  E[b; c]  E[a; c])

Definition: utrans
(basic):: UniformlyTrans(T;x,y.E[x; y]) ==  ∀[a,b,c:T].  (E[a; b]  E[b; c]  E[a; c])

Lemma: trans_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (Trans(T;x,y.E[x;y]) ∈ ℙ)

Lemma: utrans_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (UniformlyTrans(T;x,y.E[x;y]) ∈ ℙ)

Lemma: trans_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R[x;y] ⇐⇒ R'[x;y]))  (Trans(T;y,x.R[x;y]) ⇐⇒ Trans(T;y,x.R'[x;y])))

Lemma: utrans_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  (R[x;y] ⇐⇒ R'[x;y]))  (UniformlyTrans(T;y,x.R[x;y]) ⇐⇒ UniformlyTrans(T;y,x.R'[x;y])))

Lemma: trans_rel_self_functionality
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Trans(T;x,y.R[x;y])  {∀a,a',b,b':T.  (R[b;a]  R[a';b']  R[a;a']  R[b;b'])})

Lemma: utrans_rel_self_functionality
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (UniformlyTrans(T;x,y.R[x;y])  {∀[a,a',b,b':T].  (R[b;a]  R[a';b']  R[a;a']  R[b;b'])})

Definition: equiv_rel
(compound):: EquivRel(T;x,y.E[x; y]) ==  Refl(T;x,y.E[x; y]) ∧ Sym(T;x,y.E[x; y]) ∧ Trans(T;x,y.E[x; y])

Definition: uequiv_rel
UniformEquivRel(T;x,y.E[x; y]) ==
  UniformlyRefl(T;x,y.E[x; y]) ∧ UniformlySym(T;x,y.E[x; y]) ∧ UniformlyTrans(T;x,y.E[x; y])

Lemma: equiv_rel_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (EquivRel(T;x,y.E[x;y]) ∈ ℙ)

Lemma: equiv_rel_and
[T:Type]. ∀[E1,E2:T ⟶ T ⟶ ℙ].
  (EquivRel(T;x,y.E2[x;y])  EquivRel(T;x,y.E1[x;y])  EquivRel(T;x,y.E1[x;y] ∧ E2[x;y]))

Lemma: equiv_rel_true
[T:Type]. EquivRel(T;x,y.True)

Lemma: equiv_rel_squash2
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  ((↓EquivRel(T;x,y.E[x;y]))  EquivRel(T;x,y.↓E[x;y]))

Lemma: equiv_rel_squash
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (EquivRel(T;x,y.E[x;y])  EquivRel(T;x,y.↓E[x;y]))

Lemma: uequiv_rel_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (UniformEquivRel(T;x,y.E[x;y]) ∈ ℙ)

Lemma: equiv_rel_subtype
[T,S:Type]. ∀[R:T ⟶ T ⟶ Type].  EquivRel(T;x,y.R[x;y])  EquivRel(S;x,y.R[x;y]) supposing S ⊆T

Lemma: equiv_rel_isect2
[A,B:Type].  ∀E:A ⟶ A ⟶ ℙ(EquivRel(A;x,y.E[x;y])  EquivRel(A ⋂ B;x,y.E[x;y]))

Lemma: equiv_rel_subtyping
[T:Type]. ∀[R:T ⟶ T ⟶ Type]. ∀[Q:T ⟶ ℙ].  (EquivRel(T;x,y.R[x;y])  EquivRel({z:T| Q[z]} ;x,y.R[x;y]))

Lemma: uequiv_rel_subtyping
[T:Type]. ∀[R:T ⟶ T ⟶ Type]. ∀[Q:T ⟶ ℙ].  (UniformEquivRel(T;x,y.R[x;y])  UniformEquivRel({z:T| Q[z]} ;x,y.R[x;y])\000C)

Definition: preorder
(compound):: Preorder(T;x,y.R[x; y]) ==  Refl(T;x,y.R[x; y]) ∧ Trans(T;x,y.R[x; y])

Definition: upreorder
(compound):: UniformPreorder(T;x,y.R[x; y]) ==  UniformlyRefl(T;x,y.R[x; y]) ∧ UniformlyTrans(T;x,y.R[x; y])

Lemma: preorder_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Preorder(T;x,y.R[x;y]) ∈ ℙ)

Lemma: upreorder_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (UniformPreorder(T;x,y.R[x;y]) ∈ ℙ)

Comment: symmetrize_com
The ⌜𝕌{j}⌝ type for was necessary for
proving the lemma eqvtype_wf in theory
subtyping. With ⌜Type⌝the type of symmetrize
was unnecessarily tied to the type
of the arguments and b.

Definition: symmetrize
Symmetrize(x,y.R[x; y];a;b) ==  R[a; b] ∧ R[b; a]

Lemma: symmetrize_wf
[T:𝕌{j}]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[a,b:T].  (Symmetrize(x,y.R[x;y];a;b) ∈ ℙ)

Lemma: symmetrized_preorder
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Preorder(T;x,y.R[x;y])  EquivRel(T;a,b.Symmetrize(x,y.R[x;y];a;b)))

Lemma: trans_rel_func_wrt_sym_self
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
   {∀a,a',b,b':T.  (Symmetrize(x,y.R[x;y];a;b)  Symmetrize(x,y.R[x;y];a';b')  (R[a;a'] ⇐⇒ R[b;b']))})

Lemma: equiv_rel_iff
EquivRel(ℙ;A,B.A ⇐⇒ B)

Lemma: uequiv_rel_iff
UniformEquivRel(ℙ;A,B.A ⇐⇒ B)

Lemma: equiv_rel_functionality_wrt_iff
[T,T':Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀[E':T' ⟶ T' ⟶ ℙ].
  (∀x,y:T.  (E[x;y] ⇐⇒ E'[x;y]))  (EquivRel(T;x,y.E[x;y]) ⇐⇒ EquivRel(T';x,y.E'[x;y])) supposing T' ∈ Type

Lemma: uequiv_rel_functionality_wrt_iff
[T,T':Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀[E':T' ⟶ T' ⟶ ℙ].
  (∀[x,y:T].  (E[x;y] ⇐⇒ E'[x;y]))  (UniformEquivRel(T;x,y.E[x;y]) ⇐⇒ UniformEquivRel(T';x,y.E'[x;y])) 
  supposing T' ∈ Type

Comment: equiv_rel_self_fun_com
This lemma is useful for quickly proving functionality
lemmas for equivalence relations.

Lemma: equiv_rel_self_functionality
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (EquivRel(T;x,y.R[x;y])  {∀a,a',b,b':T.  (R[a;b]  R[a';b']  (R[a;a'] ⇐⇒ R[b;b']))})

Lemma: uequiv_rel_self_functionality
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (UniformEquivRel(T;x,y.R[x;y])  {∀[a,a',b,b':T].  (R[a;b]  R[a';b']  (R[a;a'] ⇐⇒ R[b;b']))})

Lemma: squash_thru_equiv_rel
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  ((↓EquivRel(T;x,y.E[x;y]))  EquivRel(T;x,y.↓E[x;y]))

Lemma: squash_thru_uequiv_rel
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  ((↓UniformEquivRel(T;x,y.E[x;y]))  UniformEquivRel(T;x,y.↓E[x;y]))

Definition: eqfun_p
(basic):: IsEqFun(T;eq) ==  ∀[x,y:T].  uiff(↑(x eq y);x y ∈ T)

Lemma: eqfun_p_wf
[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹].  (IsEqFun(T;eq) ∈ ℙ)

Lemma: sq_stable__eqfun_p
[T:Type]. ∀[eq:T ⟶ T ⟶ 𝔹].  SqStable(IsEqFun(T;eq))

Definition: anti_sym
(basic):: AntiSym(T;x,y.R[x; y]) ==  ∀x,y:T.  (R[x; y]  R[y; x]  (x y ∈ T))

Definition: uanti_sym
(basic):: UniformlyAntiSym(T;x,y.R[x; y]) ==  ∀[x,y:T].  (x y ∈ T) supposing (R[y; x] and R[x; y])

Lemma: anti_sym_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (AntiSym(T;x,y.R[x;y]) ∈ ℙ)

Lemma: uanti_sym_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (UniformlyAntiSym(T;x,y.R[x;y]) ∈ ℙ)

Lemma: anti_sym_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  uiff(AntiSym(T;x,y.R[x;y]);AntiSym(T;x,y.R'[x;y])) supposing ∀x,y:T.  (R[x;y] ⇐⇒ R'[x;y])

Lemma: uanti_sym_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  uiff(UniformlyAntiSym(T;x,y.R[x;y]);UniformlyAntiSym(T;x,y.R'[x;y])) supposing ∀[x,y:T].  (R[x;y] ⇐⇒ R'[x;y])

Definition: st_anti_sym
(basic):: StAntiSym(T;x,y.R[x; y]) ==  ∀x,y:T.  (R[x; y] ∧ R[y; x]))

Lemma: st_anti_sym_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (StAntiSym(T;x,y.R[x;y]) ∈ ℙ)

Definition: strict_part
strict_part(x,y.R[x; y];a;b) ==  R[a; b] ∧ R[b; a])

Lemma: strict_part_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[a,b:T].  (strict_part(x,y.R[x;y];a;b) ∈ ℙ)

Lemma: strict_part_irrefl
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[a,b:T].  ¬(a b ∈ T) supposing strict_part(x,y.R[x;y];a;b)

Definition: connex
(basic):: Connex(T;x,y.R[x; y]) ==  ∀x,y:T.  (R[x; y] ∨ R[y; x])

Definition: uconnex
(basic):: uconnex(T; x,y.R[x; y]) ==  ∀[x,y:T].  (R[x; y] ∨ R[y; x])

Lemma: connex_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Connex(T;x,y.R[x;y]) ∈ ℙ)

Lemma: uconnex_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (uconnex(T; x,y.R[x;y]) ∈ ℙ)

Definition: weak-connex
(basic):: weak-connex(T; x,y.R[x; y]) ==  ∀[x,y:T].  (↓R[x; y] ∨ R[y; x])

Lemma: weak-connex_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (weak-connex(T; x,y.R[x;y]) ∈ ℙ)

Lemma: connex_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R[x;y] ⇐⇒ R'[x;y]))  (Connex(T;x,y.R[x;y]) ⇐⇒ Connex(T;x,y.R'[x;y])))

Lemma: uconnex_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  (R[x;y] ⇐⇒ R'[x;y]))  (uconnex(T; x,y.R[x;y]) ⇐⇒ uconnex(T; x,y.R'[x;y])))

Lemma: connex_functionality_wrt_implies
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  {R[x;y]  R'[x;y]})  {Connex(T;x,y.R[x;y])  Connex(T;x,y.R'[x;y])})

Lemma: uconnex_functionality_wrt_implies
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  {R[x;y]  R'[x;y]})  {uconnex(T; x,y.R[x;y])  uconnex(T; x,y.R'[x;y])})

Lemma: connex_iff_trichot
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀a,b:T.  Dec(R[a;b]))
     ⇐⇒ {∀a,b:T.  (strict_part(x,y.R[x;y];a;b) ∨ Symmetrize(x,y.R[x;y];a;b) ∨ strict_part(x,y.R[x;y];b;a))}))

Lemma: uconnex_iff_trichot
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀[a,b:T].  Dec(R[a;b]))
   (uconnex(T; x,y.R[x;y])
     ⇐⇒ {∀[a,b:T].  (strict_part(x,y.R[x;y];a;b) ∨ Symmetrize(x,y.R[x;y];a;b) ∨ strict_part(x,y.R[x;y];b;a))}))

Definition: order
(compound):: Order(T;x,y.R[x; y]) ==  Refl(T;x,y.R[x; y]) ∧ Trans(T;x,y.R[x; y]) ∧ AntiSym(T;x,y.R[x; y])

Definition: uorder
UniformOrder(T;x,y.R[x; y]) ==
  UniformlyRefl(T;x,y.R[x; y]) ∧ UniformlyTrans(T;x,y.R[x; y]) ∧ UniformlyAntiSym(T;x,y.R[x; y])

Lemma: order_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Order(T;x,y.R[x;y]) ∈ ℙ)

Lemma: uorder_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (UniformOrder(T;x,y.R[x;y]) ∈ ℙ)

Lemma: order_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R[x;y] ⇐⇒ R'[x;y]))  (Order(T;x,y.R[x;y]) ⇐⇒ Order(T;x,y.R'[x;y])))

Lemma: uorder_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  (R[x;y] ⇐⇒ R'[x;y]))  (UniformOrder(T;x,y.R[x;y]) ⇐⇒ UniformOrder(T;x,y.R'[x;y])))

Definition: linorder
(compound):: Linorder(T;x,y.R[x; y]) ==  Order(T;x,y.R[x; y]) ∧ Connex(T;x,y.R[x; y])

Definition: ulinorder
UniformLinorder(T;x,y.R[x; y]) ==
  UniformOrder(T;x,y.R[x; y]) ∧ Connex(T;x,y.R[x; y]) ∧ (∀[x,y:T].  R[x; y] supposing R[x; y])

Definition: weak-linorder
(compound):: WeakLinorder(T;x,y.R[x; y]) ==  Order(T;x,y.R[x; y]) ∧ weak-connex(T; x,y.R[x; y])

Lemma: linorder_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Linorder(T;x,y.R[x;y]) ∈ ℙ)

Lemma: ulinorder_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (UniformLinorder(T;x,y.R[x;y]) ∈ ℙ)

Lemma: weak-linorder_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (WeakLinorder(T;x,y.R[x;y]) ∈ ℙ)

Lemma: linorder_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀x,y:T.  (R[x;y] ⇐⇒ R'[x;y]))  (Linorder(T;x,y.R[x;y]) ⇐⇒ Linorder(T;x,y.R'[x;y])))

Lemma: linorder_functionality_wrt_ext-eq
[A,B:Type]. ∀[R:A ⟶ A ⟶ ℙ].  Linorder(A;x,y.R[x;y]) ⇐⇒ Linorder(B;x,y.R[x;y]) supposing A ≡ B

Lemma: ulinorder_functionality_wrt_iff
[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  uiff(R[x;y];R'[x;y]))  (UniformLinorder(T;x,y.R[x;y]) ⇐⇒ UniformLinorder(T;x,y.R'[x;y])))

Lemma: sq_stable__refl
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀x,y:T.  SqStable(R[x;y]))  SqStable(Refl(T;x,y.R[x;y])))

Lemma: sq_stable__urefl
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀[x,y:T].  SqStable(R[x;y]))  SqStable(UniformlyRefl(T;x,y.R[x;y])))

Lemma: sq_stable__sym
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀x,y:T.  SqStable(R[x;y]))  SqStable(Sym(T;y,x.R[x;y])))

Lemma: sq_stable__usym
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀[x,y:T].  SqStable(R[x;y]))  SqStable(UniformlySym(T;y,x.R[x;y])))

Lemma: sq_stable__trans
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀x,y:T.  SqStable(R[x;y]))  SqStable(Trans(T;y,x.R[x;y])))

Lemma: sq_stable__utrans
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀[x,y:T].  SqStable(R[x;y]))  SqStable(UniformlyTrans(T;y,x.R[x;y])))

Lemma: sq_stable__anti_sym
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  SqStable(AntiSym(T;x,y.R[x;y]))

Lemma: sq_stable__uanti_sym
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  SqStable(UniformlyAntiSym(T;x,y.R[x;y]))

Lemma: sq_stable__connex
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀x,y:T.  Dec(R[x;y]))  SqStable(Connex(T;x,y.R[x;y])))

Lemma: sq_stable__uconnex
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀[x,y:T].  Dec(R[x;y]))  SqStable(uconnex(T; x,y.R[x;y])))

Lemma: order_split
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
   (∀x,y:T.  Dec(x y ∈ T))
   (∀a,b:T.  (R[a;b] ⇐⇒ strict_part(x,y.R[x;y];a;b) ∨ (a b ∈ T))))

Lemma: uorder_split
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
   (∀[x,y:T].  Dec(x y ∈ T))
   (∀[a,b:T].  (R[a;b] ⇐⇒ strict_part(x,y.R[x;y];a;b) ∨ (a b ∈ T))))

Definition: irrefl
(basic):: Irrefl(T;x,y.E[x; y]) ==  ∀[a:T]. E[a; a])

Lemma: irrefl_wf
[T:Type]. ∀[E:T ⟶ T ⟶ ℙ].  (Irrefl(T;x,y.E[x;y]) ∈ ℙ)

Lemma: trans_imp_sp_trans
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Trans(T;a,b.R[a;b])  Trans(T;a,b.strict_part(x,y.R[x;y];a;b)))

Lemma: utrans_imp_sp_utrans
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (UniformlyTrans(T;a,b.R[a;b])  UniformlyTrans(T;a,b.strict_part(x,y.R[x;y];a;b)))

Lemma: trans_imp_sp_trans_a
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (Trans(T;a,b.R[a;b])  {∀a,b,c:T.  (R[a;b]  strict_part(x,y.R[x;y];b;c)  strict_part(x,y.R[x;y];a;c))})

Lemma: utrans_imp_sp_utrans_a
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  R[x;y] supposing R[x;y])
   {∀[a,b,c:T].  (strict_part(x,y.R[x;y];a;c)) supposing (strict_part(x,y.R[x;y];b;c) and R[a;b])})

Lemma: trans_imp_sp_trans_b
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (Trans(T;a,b.R[a;b])  {∀a,b,c:T.  (strict_part(x,y.R[x;y];a;b)  R[b;c]  strict_part(x,y.R[x;y];a;c))})

Lemma: utrans_imp_sp_utrans_b
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀[x,y:T].  R[x;y] supposing R[x;y])
   {∀[a,b,c:T].  (strict_part(x,y.R[x;y];a;c)) supposing (strict_part(x,y.R[x;y];a;b) and R[b;c])})

Lemma: linorder_le_neg
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (Linorder(T;x,y.R[x;y])  (∀a,b:T.  R[a;b] ⇐⇒ strict_part(x,y.R[x;y];b;a))))

Lemma: ulinorder_le_neg
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (UniformLinorder(T;x,y.R[x;y])  (∀[a,b:T].  uiff(¬R[a;b];strict_part(x,y.R[x;y];b;a))))

Lemma: linorder_lt_neg
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀x,y:T.  Dec(R[x;y]))  Linorder(T;x,y.R[x;y])  (∀a,b:T.  strict_part(x,y.R[x;y];a;b) ⇐⇒ R[b;a])))

Lemma: ulinorder_lt_neg
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀x,y:T.  Dec(R[x;y]))  UniformLinorder(T;x,y.R[x;y])  (∀[a,b:T].  uiff(¬strict_part(x,y.R[x;y];a;b);R[b;a])))

Lemma: pair-order
[A,B:Type]. ∀[Ra:A ⟶ A ⟶ ℙ]. ∀[Rb:B ⟶ B ⟶ ℙ].
   Order(A × B;x,y.Ra[fst(x);fst(y)] ∧ ((¬((fst(x)) (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)])))

Lemma: locally-ranked-is-well-founded
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
   (∀k:ℕ. ∀rank:T ⟶ ℕ. ∀l:T ⟶ ℕk.
        ((∀x,y:T.  (((l x) (l y) ∈ ℤ R[x;y]  rank x < rank y))  tcWO(T;x,y.R[y;x]))))

Lemma: locally-ranked-induction
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
   (∀k:ℕ. ∀rank:T ⟶ ℕ. ∀l:T ⟶ ℕk.
        ((∀x,y:T.  (((l x) (l y) ∈ ℤ R[x;y]  rank x < rank y))  (∀[Q:T ⟶ ℙ]. TI(T;x,y.R[y;x];x.Q[x])))))

Definition: least-upper-bound
least-upper-bound(T;x,y.R[x; y];a;b;c) ==  R[a; c] ∧ R[b; c] ∧ (∀x:T. (R[a; x]  R[b; x]  R[c; x]))

Lemma: least-upper-bound_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[a,b,c:T].  (least-upper-bound(T;x,y.R[x;y];a;b;c) ∈ ℙ)

Lemma: least-upper-bound-unique
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    (c d ∈ T) supposing (least-upper-bound(T;x,y.R[x;y];a;b;c) and least-upper-bound(T;x,y.R[x;y];a;b;d)) 
  supposing Order(T;x,y.R[x;y])

Lemma: least-upper-bound-com
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    (c d ∈ T) supposing (least-upper-bound(T;x,y.R[x;y];a;b;c) and least-upper-bound(T;x,y.R[x;y];b;a;d)) 
  supposing Order(T;x,y.R[x;y])

Lemma: lub-com
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀[lub:T ⟶ T ⟶ T]
    ∀[a,b:T].  ((lub b) (lub a) ∈ T) supposing ∀[a,b:T].  least-upper-bound(T;x,y.R[x;y];a;b;lub b) 
  supposing Order(T;x,y.R[x;y])

Lemma: least-upper-bound-assoc
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    (u1 u2 ∈ T) supposing 
       (least-upper-bound(T;x,y.R[x;y];a;b;x) and 
       least-upper-bound(T;x,y.R[x;y];x;c;u1) and 
       least-upper-bound(T;x,y.R[x;y];b;c;y) and 
  supposing Order(T;x,y.R[x;y])

Lemma: lub-assoc
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀[lub:T ⟶ T ⟶ T]
    ∀[a,b,c:T].  ((lub (lub c)) (lub (lub b) c) ∈ T) 
    supposing ∀[a,b:T].  least-upper-bound(T;x,y.R[x;y];a;b;lub b) 
  supposing Order(T;x,y.R[x;y])

Definition: greatest-lower-bound
greatest-lower-bound(T;x,y.R[x; y];a;b;c) ==  R[c; a] ∧ R[c; b] ∧ (∀x:T. (R[x; a]  R[x; b]  R[x; c]))

Lemma: greatest-lower-bound_wf
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[a,b,c:T].  (greatest-lower-bound(T;x,y.R[x;y];a;b;c) ∈ ℙ)

Lemma: greatest-lower-bound-unique
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    (c d ∈ T) supposing (greatest-lower-bound(T;x,y.R[x;y];a;b;c) and greatest-lower-bound(T;x,y.R[x;y];a;b;d)) 
  supposing Order(T;x,y.R[x;y])

Lemma: greatest-lower-bound-com
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    (c d ∈ T) supposing (greatest-lower-bound(T;x,y.R[x;y];a;b;c) and greatest-lower-bound(T;x,y.R[x;y];b;a;d)) 
  supposing Order(T;x,y.R[x;y])

Lemma: glb-com
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀[glb:T ⟶ T ⟶ T]
    ∀[a,b:T].  ((glb b) (glb a) ∈ T) supposing ∀[a,b:T].  greatest-lower-bound(T;x,y.R[x;y];a;b;glb b) 
  supposing Order(T;x,y.R[x;y])

Lemma: greatest-lower-bound-assoc
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    (u1 u2 ∈ T) supposing 
       (greatest-lower-bound(T;x,y.R[x;y];a;b;x) and 
       greatest-lower-bound(T;x,y.R[x;y];x;c;u1) and 
       greatest-lower-bound(T;x,y.R[x;y];b;c;y) and 
  supposing Order(T;x,y.R[x;y])

Lemma: glb-assoc
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀[glb:T ⟶ T ⟶ T]
    ∀[a,b,c:T].  ((glb (glb c)) (glb (glb b) c) ∈ T) 
    supposing ∀[a,b:T].  greatest-lower-bound(T;x,y.R[x;y];a;b;glb b) 
  supposing Order(T;x,y.R[x;y])

Definition: approx-per
approx-per(T;x;y) ==
  ((∃t:Base. ((x ≤ t) ∧ (t ∈ T))) ∧ (∃t:Base. ((y ≤ t) ∧ (t ∈ T))))
  ∧ (∀t:Base. (((x ≤ t) ∧ (t ∈ T))  (∃t':Base. ((y ≤ t') ∧ (t' t ∈ T)))))
  ∧ (∀t:Base. (((y ≤ t) ∧ (t ∈ T))  (∃t':Base. ((x ≤ t') ∧ (t' t ∈ T)))))

Lemma: approx-per_wf
[T:Type]. ∀[x,y:Base].  (approx-per(T;x;y) ∈ ℙ)

Lemma: approx-per-trans
[T:Type]. Trans(Base;x,y.approx-per(T;x;y))

Lemma: approx-per-for-mono
[T:Type]. ∀x,y:Base.  approx-per(T;x;y) supposing y ∈ supposing mono(T)

Lemma: approx-per-for-base
[T:Type]. ∀x,y:Base.  approx-per(T;x;y) supposing y ∈ supposing T ⊆Base

Lemma: member-eq-is-equiv
[A,B:Type].  EquivRel(A;x,y.(x ∈ B) (y ∈ B) ∈ Type) supposing respects-equality(A;B)

Lemma: sorted-seq-iff
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀s:sequence(T). (Trans(T;x,y.R[x;y])  (sorted-seq(x,y.R[x;y];s) ⇐⇒ ∀i:ℕ||s|| 1. R[s[i];s[i 1]]))

Home Index