Theory: relations2

Definition: rel_path
rel_path(A;L;x;y) ==

  rec-case(L) of [] => λx,y. (x = y ∈ A) | a::as => rec.λx,y. (((fst(a)) = x ∈ A) ∧ (rec (fst(snd(a))) y)) x y

Lemma: rel_path_wf

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ]. ∀[x,y:A]. ∀[L:(a:A × b:A × (R a b)) List].  (rel_path(A;L;x;y) ∈ ℙ)

Lemma: sq_stable__rel_path

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀L:(a:A × b:A × (R a b)) List. ∀[x,y:A].  SqStable(rel_path(A;L;x;y))

Lemma: rel_path-append
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].

  ∀L:(a:A × b:A × (R a b)) List. ∀x,y,z:A. ∀r:R y z.  rel_path(A;L @ [<y, z, r>];x;z) supposing rel_path(A;L;x;y)

Definition: transitive-closure
TC(R) ==  λx,y. {L:(a:A × b:A × (R a b)) List| rel_path(A;L;x;y) ∧ 0 < ||L||}

Lemma: transitive-closure_wf
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (TC(R) ∈ A ⟶ A ⟶ ℙ)

Lemma: transitive-closure-map
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].
  ∀f:A ⟶ A. ((∀x,y:A.  ((R x y) ⇒ (R (f x) (f y)))) ⇒ (∀x,y:A.  ((TC(R) x y) ⇒ (TC(R) (f x) (f y)))))

Lemma: transitive-closure-transitive
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  UniformlyTrans(A;x,y.x TC(R) y)

Lemma: transitive-closure-symmetric
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (Sym(A;x,y.R x y) ⇒ Sym(A;x,y.x TC(R) y))

Lemma: transitive-closure-cases
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y:A.  ((x TC(R) y) ⇒ ((x R y) ∨ (∃z:A. ((x R z) ∧ (z TC(R) y)))))

Lemma: transitive-closure-contains
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  R => TC(R)

Lemma: transitive-closure-minimal
∀[A:Type]. ∀[R,Q:A ⟶ A ⟶ ℙ].  (R => Q ⇒ Trans(A;x,y.x Q y) ⇒ TC(R) => Q)

Lemma: transitive-closure-minimal-uniform
∀[A:Type]. ∀[R,Q:A ⟶ A ⟶ ℙ].  (R => Q ⇒ UniformlyTrans(A;x,y.x Q y) ⇒ TC(R) => Q)

Lemma: transitive-closure-minimal-ext
∀[A:Type]. ∀[R,Q:A ⟶ A ⟶ ℙ].  (R => Q ⇒ Trans(A;x,y.x Q y) ⇒ TC(R) => Q)

Lemma: transitive-closure-induction
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[R:A ⟶ A ⟶ ℙ].
  ((∀x,y:A.  ((x R y) ⇒ P[x] ⇒ P[y])) ⇒ (∀x,y:A.  ((x TC(R) y) ⇒ P[x] ⇒ P[y])))

Lemma: transitive-closure-induction-ext
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[R:A ⟶ A ⟶ ℙ].
  ((∀x,y:A.  ((x R y) ⇒ P[x] ⇒ P[y])) ⇒ (∀x,y:A.  ((x TC(R) y) ⇒ P[x] ⇒ P[y])))

Definition: transitive-reflexive-closure
R^* ==  λx,y. ((x = y ∈ A) ∨ (TC(R) x y))

Lemma: transitive-reflexive-closure_wf
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (R^* ∈ A ⟶ A ⟶ ℙ)

Lemma: transitive-reflexive-closure-cases
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y:A.  ((x R^* y) ⇒ ((x = y ∈ A) ∨ (∃z:A. ((x R z) ∧ (z R^* y)))))

Lemma: transitive-reflexive-closure_transitivity
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y,z:A.  ((x R^* y) ⇒ (y R^* z) ⇒ (x R^* z))

Lemma: transitive-reflexive-closure-base-case
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  ∀x,y:A.  ((x R y) ⇒ (x R^* y))

Lemma: transitive-reflexive-closure-map
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].
  ∀f:A ⟶ A. ((∀x,y:A.  ((R x y) ⇒ (R (f x) (f y)))) ⇒ (∀x,y:A.  ((R^* x y) ⇒ (R^* (f x) (f y)))))

Definition: rel-diamond-property
rel-diamond-property(T;x,y.R[x; y]) ==  ∀x,y,z:T.  (R[x; y] ⇒ R[x; z] ⇒ ((y = z ∈ T) ∨ (∃w:T. (R[y; w] ∧ R[z; w]))))

Lemma: rel-diamond-property_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (rel-diamond-property(T;x,y.R[x;y]) ∈ ℙ)

Definition: rel-confluent
rel-confluent(T;x,y.R[x; y]) ==  ∀x,y,z:T.  (R[x; y] ⇒ R[x; z] ⇒ (∃w:T. (R[y; w] ∧ R[z; w])))

Lemma: rel-confluent_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (rel-confluent(T;x,y.R[x;y]) ∈ ℙ)

Lemma: diamond-implies-TC-confluent
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (rel-diamond-property(T;x,y.R[x;y])
  ⇒ (∃m:T ⟶ ℕ. ∀x,y:T.  (R[x;y] ⇒ m y < m x))
  ⇒ rel-confluent(T;x,y.λx,y. R[x;y]^* x y))

Definition: confluent-equiv
confluent-equiv(T;x,y.R[x; y]) ==  λa,b. ∃w:T. (R[a; w] ∧ R[b; w])

Lemma: confluent-equiv_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (confluent-equiv(T;x,y.R[x;y]) ∈ T ⟶ T ⟶ ℙ)

Lemma: confluent-equiv-is-equiv
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (Refl(T;x,y.R[x;y])
  ⇒ Trans(T;x,y.R[x;y])
  ⇒ rel-confluent(T;x,y.R[x;y])
  ⇒ EquivRel(T;a,b.confluent-equiv(T;x,y.R[x;y]) a b))

Lemma: TC-equiv-is-equiv
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (rel-diamond-property(T;x,y.R x y)
  ⇒ (∃m:T ⟶ ℕ. ∀x,y:T.  ((R x y) ⇒ m y < m x))
  ⇒ EquivRel(T;a,b.confluent-equiv(T;x,y.R^* x y) a b))

Definition: least-equiv
least-equiv(A;R) ==  λx,y. ((R x y) ∨ (R y x))^*

Lemma: least-equiv_wf
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (least-equiv(A;R) ∈ A ⟶ A ⟶ ℙ)

Lemma: least-equiv-is-equiv-1
∀[A,B:Type].  ∀[R:B ⟶ B ⟶ ℙ]. EquivRel(A;x,y.least-equiv(B;R) x y) supposing A ⊆r B

Lemma: least-equiv-is-equiv
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  EquivRel(A;x,y.least-equiv(A;R) x y)

Lemma: implies-least-equiv
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  R => least-equiv(A;R)

Lemma: least-equiv-implies
∀[A:Type]. ∀[R,E:A ⟶ A ⟶ ℙ].  (R => E ⇒ EquivRel(A;x,y.E x y) ⇒ least-equiv(A;R) => E)

Lemma: least-equiv-cases
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].
  ∀a,b:A.
    ((least-equiv(A;R) a b)
    ⇒

 ((a = b ∈ A) ∨ ((R a b) ∨ (R b a)) ∨ (∃c:A. (((R c b) ∨ (R b c)) ∧ (least-equiv(A;R) a c)))))

Lemma: least-equiv-cases2
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].
  ∀a,b:A.
    ((least-equiv(A;R) a b)
    ⇒

 ((a = b ∈ A) ∨ ((R a b) ∨ (R b a)) ∨ (∃c:A. (((R a c) ∨ (R c a)) ∧ (least-equiv(A;R) c b)))))

Lemma: least-equiv-induction
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀[R:A ⟶ A ⟶ ℙ].
  ((∀x,y:A.  ((x R y) ⇒ (P[x] ⇐⇒ P[y]))) ⇒ (∀x,y:A.  ((x least-equiv(A;R) y) ⇒ P[x] ⇒ P[y])))

Lemma: least-equiv-induction2
∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].
  ∀x,y:A.  ((x least-equiv(A;R) y) ⇒ {∀[P:A ⟶ ℙ]. ((∀x,y:A.  ((x R y) ⇒ (P[x] ⇐⇒ P[y]))) ⇒ P[x] ⇒ P[y])})

Definition: imp-type
imp-type(A;B) ==  x,y:Base//(least-equiv(Base;λx,y. ((x = y ∈ A) ⇒ (x = y ∈ B))) x y)

Lemma: imp-type_wf
∀[A,B:Type].  (imp-type(A;B) ∈ Type)

Lemma: subtype_imp-type
∀[A,B:Type].  (B ⊆r imp-type(A;B))

Definition: rel_plus
R⁺ ==  λx,y. ∃n:ℕ⁺. (x R^n y)

Lemma: rel_plus_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ Type].  (R⁺ ∈ T ⟶ T ⟶ Type)

Lemma: implies-rel_plus
∀[T:Type]. ∀[R:T ⟶ T ⟶ Type]. ∀[x:T].  ∀y:T. ((R x y) ⇒ (R⁺ x y))

Lemma: rel_plus_transitivity
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[x,y,z:T].  ((R⁺ x y) ⇒ (R⁺ y z) ⇒ (R⁺ x z))

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

Lemma: rel_plus_implies
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  ((x R⁺ y) ⇒ ((x R y) ∨ (∃z:T. ((x R⁺ z) ∧ (z R y)))))

Lemma: rel_plus_implies2
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  ((x R⁺ y) ⇒ ((x R y) ∨ (∃z:T. ((x R z) ∧ (z R⁺ y)))))

Definition: rel_finite
rel_finite(T;R) ==  ∀x:T. ∃L:T List. ∀z:T. ((z R x) ⇒ (z ∈ L))

Lemma: rel_finite_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (rel_finite(T;R) ∈ ℙ)

Lemma: rel_finite-restrict
∀[E:Type]. ∀P:E ⟶ 𝔹. ∀[R:E ⟶ E ⟶ ℙ]. (rel_finite(E;R) ⇒ rel_finite({e:E| ↑(P e)} ;R))

Lemma: rel_exp_iff
∀n:ℕ
  ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    ∀x,y:T.  (x R^n y ⇐⇒ (∃z:T. (0 < n c∧ ((x R^n - 1 z) ∧ (z R y)))) ∨ ((n = 0 ∈ ℤ) ∧ (x = y ∈ T)))

Lemma: rel_exp_iff2
∀n:ℕ
  ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
    ∀x,y:T.  (x R^n y ⇐⇒ (∃z:T. (0 < n c∧ ((x R z) ∧ (z R^n - 1 y)))) ∨ ((n = 0 ∈ ℤ) ∧ (x = y ∈ T)))

Lemma: rel_exp0
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x R^0 y ⇐⇒ x = y ∈ T)

Lemma: decidable__rel_exp_finite
∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀[R:T ⟶ T ⟶ ℙ]. (rel_finite(T;R) ⇒ (∀x,y:T.  Dec(x R y)) ⇒ (∀k:ℕ. ∀x,y:T.  Dec(x R^k y)))))

Definition: strongwellfounded
SWellFounded(R[x; y]) ==  ∃f:T ⟶ ℕ. ∀x,y:T.  (R[x; y] ⇒ f x < f y)

Lemma: strongwellfounded_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ Type].  (SWellFounded(R[x;y]) ∈ ℙ)

Lemma: strongwf-implies
∀[T:Type]. ∀[R:T ⟶ T ⟶ Type].  (SWellFounded(R[x;y]) ⇒ WellFnd{i}(T;x,y.R[x;y]))

Lemma: strongwf-monotone
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ Type].  (R2 => R1 ⇒ SWellFounded(R1[x;y]) ⇒ SWellFounded(R2[x;y]))

Lemma: rel_plus_strongwellfounded
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (SWellFounded(x R y) ⇒ SWellFounded(x R⁺ y))

Lemma: strongwellfounded_rel_exp
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[swf:SWellFounded(x R y)]. ∀[n:ℕ⁺]. ∀[x,y:T].
  (((fst(swf)) x) + n) ≤ ((fst(swf)) y) supposing x R^n y

Lemma: decidable__rel_plus
∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀[R:T ⟶ T ⟶ ℙ]. (SWellFounded(x R y) ⇒ rel_finite(T;R) ⇒ (∀x,y:T.  Dec(x R y)) ⇒ (∀x,y:T.  Dec(x R⁺ y)))))

Lemma: rel_exp_one
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x R^1 y ⇐⇒ x R y)

Lemma: rel_plus_closure
∀[T:Type]. ∀[R,R2:T ⟶ T ⟶ ℙ].
  (Trans(T)(R2[_1;_2]) ⇒ (∀x,y:T.  ((x R y) ⇒ (x R2 y))) ⇒ (∀x,y:T.  ((x R⁺ y) ⇒ (x R2 y))))

Lemma: rel_star_iff
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x (R^*) y ⇐⇒ (∃z:T. ((x (R^*) z) ∧ (z R y))) ∨ (x = y ∈ T))

Lemma: rel_star_iff2
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x (R^*) y ⇐⇒ (∃z:T. ((x R z) ∧ (z (R^*) y))) ∨ (x = y ∈ T))

Lemma: rel-star-iff-rel-plus-or
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x (R^*) y ⇐⇒ (x R⁺ y) ∨ (x = y ∈ T))

Lemma: rel-plus-implies-rel-star
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  ((x R⁺ y) ⇒ (x (R^*) y))

Definition: rel-path
rel-path(R;L) ==  ∀i:ℕ||L|| - 1. (L[i] R L[i + 1])

Lemma: rel-path_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[L:T List].  (rel-path(R;L) ∈ ℙ)

Definition: rel-path-between

rel-path-between(T;R;x;y;L) ==  rel-path(R;L) ∧ 0 < ||L|| ∧ (x = hd(L) ∈ T) ∧ (y = last(L) ∈ T)

Lemma: rel-path-between_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[L:T List]. ∀[x,y:T].  (rel-path-between(T;R;x;y;L) ∈ ℙ)

Lemma: rel-path-between-cons
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀L:T List. ∀x,y,z:T.
    (rel-path-between(T;R;x;y;[z / L])
    ⇐⇒

 (x = z ∈ T) ∧ y = z ∈ T supposing ↑null(L) ∧ (x R hd(L)) ∧ rel-path-between(T;R;hd(L);y;L) supposing ¬↑null(L))

Lemma: rel-path-between-append
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀L1,L2:T List. ∀x,y,z:T.
    (rel-path-between(T;R;x;y;L1)
    ⇒ rel-path-between(T;R;y;z;L2)
    ⇒ Refl(T;v1,v2.R v1 v2)
    ⇒ rel-path-between(T;R;x;z;L1 @ L2))

Lemma: rel_exp-iff-path
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀n:ℕ. ∀x,y:T.  (x R^n y ⇐⇒ ∃L:T List. ((||L|| = (n + 1) ∈ ℤ) ∧ rel-path-between(T;R;x;y;L)))

Lemma: rel_star-iff-path
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x (R^*) y ⇐⇒ ∃L:T List. rel-path-between(T;R;x;y;L))

Lemma: rel_plus-iff-path
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x R⁺ y ⇐⇒ ∃L:T List. (1 < ||L|| ∧ rel-path-between(T;R;x;y;L)))

Definition: acyclic-rel
acyclic-rel(T;R) ==  ∀x:T. (¬(x R⁺ x))

Lemma: acyclic-rel_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (acyclic-rel(T;R) ∈ ℙ)

Lemma: wellfounded-acyclic-rel
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (SWellFounded(x R y) ⇒ acyclic-rel(T;R))

Lemma: rel-rel-plus
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  ((x R y) ⇒ (x R⁺ y))

Lemma: rel-star-rel-plus
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y,z:T.  ((x (R^*) y) ⇒ (y R z) ⇒ (x R⁺ z))

Lemma: rel-star-rel-plus2
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y,z:T.  ((x R y) ⇒ (y (R^*) z) ⇒ (x R⁺ z))

Lemma: rel-star-rel-plus3
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y,z:T.  ((x (R^*) y) ⇒ (y R⁺ z) ⇒ (x R⁺ z))

Lemma: rel-plus-rel-star
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  ((x R⁺ y) ⇒ (x (R^*) y))

Lemma: rel-star-iff-rel-plus
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (x (R^*) y ⇐⇒ (x R⁺ y) ∨ (x = y ∈ T))

Lemma: rel_plus_iff
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,z:T.  (x R⁺ z ⇐⇒ ∃y:T. ((x (R^*) y) ∧ (y R z)))

Lemma: rel_plus_iff2
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,z:T.  (x R⁺ z ⇐⇒ ∃y:T. ((x R y) ∧ (y (R^*) z)))

Lemma: rel_plus_monotone
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 ⇒ R1⁺ => R2⁺)

Lemma: rel_plus_irreflexive
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (WellFnd{i}(T;x,y.x R y) ⇒ (∀x:T. (¬(x R⁺ x))))

Lemma: rel_star_order
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (WellFnd{i}(T;x,y.x R y) ⇒ Order(T;x,y.x (R^*) y))

Lemma: rel_plus_functionality_wrt_rel_implies
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 ⇒ R1⁺ => R2⁺)

Lemma: rel_plus-weak-TI
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  (∀Q:T ⟶ ℙ. weak-TI(T;x,y.R[x;y];x.Q[x]) ⇐⇒ ∀Q:T ⟶ ℙ. weak-TI(T;x,y.R⁺ x y;x.Q[x]))

Lemma: rel_plus-TI
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  ((∀Q:T ⟶ ℙ. TI(T;x,y.R⁺ x y;x.Q[x])) ⇒ (∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];x.Q[x])))

Lemma: rel_plus-uniform-TI
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.  ((∀Q:T ⟶ ℙ. uniform-TI(T;x,y.R⁺ x y;x.Q[x])) ⇒ (∀Q:T ⟶ ℙ. uniform-TI(T;x,y.R[x;y];x.Q[x])))

Lemma: AF-induction4
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.

  ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t]) supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R⁺[x;y]

⇒ (¬R'[x;y]))))

Lemma: AF-induction-iff
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  ((∀x,y:T.  Dec(R⁺[x;y]))
  ⇒ (∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R⁺[x;y] ⇒ (¬R'[x;y])))) ⇐⇒ ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t])))

Lemma: AF-uniform-induction4
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  ∀Q:T ⟶ ℙ. uniform-TI(T;x,y.R[x;y];t.Q[t])
  supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R⁺[x;y] ⇒ (¬R'[x;y]))))

Lemma: AF-uniform-induction4-ext
∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  ∀Q:T ⟶ ℙ. uniform-TI(T;x,y.R[x;y];t.Q[t])
  supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R⁺[x;y] ⇒ (¬R'[x;y]))))

Lemma: rel_star_functionality_wrt_rel_implies
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 ⇒ R1^* => R2^*)

Lemma: rel_exp_functionality_wrt_rel_implies
∀n:ℕ. ∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 => R2 ⇒ R1^n => R2^n)

Definition: binrel_eqv
E <≡>{T} E' ==  ∀x,y:T.  (E x y ⇐⇒ E' x y)

Lemma: binrel_eqv_wf
∀[T:Type]. ∀[E,E':T ⟶ T ⟶ ℙ].  (E <≡>{T} E' ∈ ℙ)

Lemma: binrel_eqv_transitivity
∀[T:Type]. ∀[Q,R,S:T ⟶ T ⟶ ℙ].  ((Q <≡>{T} R) ⇒ (R <≡>{T} S) ⇒ (Q <≡>{T} S))

Lemma: binrel_eqv_weakening
∀[T:Type]. ∀[E,E':T ⟶ T ⟶ ℙ].  E <≡>{T} E' supposing E = E' ∈ (T ⟶ T ⟶ ℙ)

Lemma: binrel_eqv_inversion
∀[T:Type]. ∀[r,r':T ⟶ T ⟶ ℙ].  ((r <≡>{T} r') ⇒ (r' <≡>{T} r))

Lemma: binrel_eqv_functionality_wrt_breqv
∀[T:Type]. ∀[a,a',b,b':T ⟶ T ⟶ ℙ].  ((a <≡>{T} b) ⇒ (a' <≡>{T} b') ⇒ (a <≡>{T} a' ⇐⇒ b <≡>{T} b'))

Definition: binrel_le
E ≡>{T} E' ==  ∀x,y:T.  ((E x y) ⇒ (E' x y))

Lemma: binrel_le_wf
∀[T:Type]. ∀[E,E':T ⟶ T ⟶ ℙ].  (E ≡>{T} E' ∈ ℙ)

Lemma: binrel_le_antisymmetry
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R ≡>{T} R') ⇒ (R' ≡>{T} R) ⇒ (R <≡>{T} R'))

Lemma: binrel_le_transitivity
∀[T:Type]. ∀[Q,R,S:T ⟶ T ⟶ ℙ].  ((Q ≡>{T} R) ⇒ (R ≡>{T} S) ⇒ (Q ≡>{T} S))

Lemma: binrel_le_weakening
∀[T:Type]. ∀[R,R':T ⟶ T ⟶ ℙ].  ((R <≡>{T} R') ⇒ (R ≡>{T} R'))

Lemma: rel_plus_functionality_wrt_brle
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 ≡>{T} R2) ⇒ (R1⁺ ≡>{T} R2⁺))

Lemma: rel_star_functionality_wrt_brle
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 ≡>{T} R2) ⇒ ((R1^*) ≡>{T} (R2^*)))

Lemma: rel_exp_functionality_wrt_brle
∀n:ℕ. ∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 ≡>{T} R2) ⇒ (R1^n ≡>{T} R2^n))

Lemma: rel_plus_functionality_wrt_breqv
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 <≡>{T} R2) ⇒ (R1⁺ <≡>{T} R2⁺))

Lemma: rel_star_functionality_wrt_breqv
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 <≡>{T} R2) ⇒ ((R1^*) <≡>{T} (R2^*)))

Lemma: rel_exp_functionality_wrt_breqv
∀n:ℕ. ∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  ((R1 <≡>{T} R2) ⇒ (R1^n <≡>{T} R2^n))

Lemma: rel_plus_minimal
∀[T:Type]. ∀[R,Q:T ⟶ T ⟶ ℙ].  (R => Q ⇒ Trans(T;x,y.x Q y) ⇒ R⁺ => Q)

Lemma: rel_plus_idempotent
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀x,y:T.  (R⁺ x y ⇐⇒ R⁺⁺ x y)

Lemma: rel_exp_functionality_wrt_iff
∀[T:Type]. ∀[R,Q:T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R x y ⇐⇒ Q x y)) ⇒ (∀n:ℕ. ∀x,y:T.  (R^n x y ⇐⇒ Q^n x y)))

Lemma: rel_plus_functionality_wrt_iff
∀[T:Type]. ∀[R,Q:T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R x y ⇐⇒ Q x y)) ⇒ (∀x,y:T.  (R⁺ x y ⇐⇒ Q⁺ x y)))

Lemma: rel_plus_field
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].
  ((∀x,y:T.  ((R x y) ⇒ ((P x) ∧ (P y)))) ⇒ (∀x,y:T.  ((R⁺ x y) ⇒ ((P x) ∧ (P y)))))

Lemma: rel_plus-of-restriction
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].  R|P⁺ => R⁺|P

Lemma: rel_plus-restriction-equiv
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].  ((∀x,y:T.  ((P[y] ∧ (R x y)) ⇒ P[x])) ⇒ (∀x,y:T.  (R|P⁺ x y ⇐⇒ R⁺|P x y)))

Definition: one-one
one-one(A;B;R) ==  ∀x:A. ∀y,z:B.  ((R x y) ⇒ (R x z) ⇒ (y = z ∈ B))

Lemma: one-one_wf
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].  (one-one(A;B;R) ∈ ℙ)

Lemma: rel_exp-one-one
∀[B:Type]. ∀[R:B ⟶ B ⟶ ℙ].  ∀[n:ℕ]. one-one(B;B;R^n) supposing one-one(B;B;R)

Lemma: rel-exp-add-iff
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀a,b:ℕ. ∀x,z:T.  (x R^a + b z ⇐⇒ ∃y:T. ((x R^a y) ∧ (y R^b z)))

Lemma: rel-exp-add-1-iff
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀a:ℕ⁺. ∀x,z:T.  (x R^a z ⇐⇒ ∃y:T. ((x R^a - 1 y) ∧ (y R z)))

Lemma: rel_or-restriction
∀[T:Type]. ∀[P,Q:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ ℙ].  R|P ∨ R|Q => R|P ∨ Q

Lemma: rel_or_idempotent
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  R ∨ R ⇐⇒ R

Definition: image-per

image-per(A;f) ==  λx,y. usquash(TC(λx,y. ∃a,b:Base. ((a = b ∈ A) ∧ (x ~ f a) ∧ (y ~ f b))) x y)

Lemma: image-per_wf
∀[A:Type]. ∀[f:Base].  (image-per(A;f) ∈ Base ⟶ Base ⟶ ℙ)

Lemma: image-per-transitive
∀[A:Type]. ∀[f:Base].  Trans(Base;x,y.image-per(A;f) x y)

Lemma: image-per-symmetric
∀[A:Type]. ∀[f:Base].  Sym(Base;x,y.image-per(A;f) x y)

Definition: imagetype
imagetype(A;f) ==  pertype(image-per(A;f))

Lemma: imagetype_wf
∀[A:Type]. ∀[f:Base].  (imagetype(A;f) ∈ Type)

Home Index