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
================
BINARY RELATIONS
================
There is a 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 x) (higher order)
or
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
R 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 I think ultimately more
desirable.
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
(compound)::
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 ⊆r 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 T 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 a 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 ⟶ ℙ].
(Trans(T;x,y.R[x;y])
⇒ {∀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 = 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 = 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]))
⇒ (Connex(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))}))
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
(compound)::
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
(compound)::
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 ⟶ ℙ].
(Order(T;x,y.R[x;y])
⇒ (∀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 ⟶ ℙ].
(UniformOrder(T;x,y.R[x;y])
⇒ (∀[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])
⇒ UniformlyTrans(T;a,b.R[a;b])
⇒ {∀[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])
⇒ UniformlyTrans(T;a,b.R[a;b])
⇒ {∀[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;a,a'.Ra[a;a'])
⇒ Order(B;b,b'.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 ⟶ ℙ].
(Trans(T;x,y.R[y;x])
⇒ (∀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 ⟶ ℙ].
(Trans(T;x,y.R[y;x])
⇒ (∀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 ⟶ ℙ].
∀[a,b,c,d: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 ⟶ ℙ].
∀[a,b,c,d: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 a b) = (lub b a) ∈ T) supposing ∀[a,b:T]. least-upper-bound(T;x,y.R[x;y];a;b;lub a b)
supposing Order(T;x,y.R[x;y])
Lemma: least-upper-bound-assoc
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀[a,b,c,x,y,u1,u2: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
least-upper-bound(T;x,y.R[x;y];a;y;u2))
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 a (lub b c)) = (lub (lub a b) c) ∈ T)
supposing ∀[a,b:T]. least-upper-bound(T;x,y.R[x;y];a;b;lub a 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 ⟶ ℙ].
∀[a,b,c,d: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 ⟶ ℙ].
∀[a,b,c,d: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 a b) = (glb b a) ∈ T) supposing ∀[a,b:T]. greatest-lower-bound(T;x,y.R[x;y];a;b;glb a b)
supposing Order(T;x,y.R[x;y])
Lemma: greatest-lower-bound-assoc
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀[a,b,c,x,y,u1,u2: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
greatest-lower-bound(T;x,y.R[x;y];a;y;u2))
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 a (glb b c)) = (glb (glb a b) c) ∈ T)
supposing ∀[a,b:T]. greatest-lower-bound(T;x,y.R[x;y];a;b;glb a 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 x = y ∈ T supposing mono(T)
Lemma: approx-per-for-base
∀[T:Type]. ∀x,y:Base. approx-per(T;x;y) supposing x = y ∈ T supposing T ⊆r 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