Definition: rel_exp
R^n == fix((λrel_exp,n. if (n =z 0) then λx,y. (x = y ∈ T) else λx,y. ∃z:T. ((x R z) ∧ (z (rel_exp (n - 1)) y)) fi )) n
Lemma: rel_exp_wf
∀[n:ℕ]. ∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (R^n ∈ T ⟶ T ⟶ ℙ)
Lemma: decidable__rel_exp
∀k,n:ℕ. ∀[R:ℕn ⟶ ℕn ⟶ ℙ]. ((∀i,j:ℕn. Dec(i R j)) ⇒ (∀i,j:ℕn. Dec(i R^k j)))
Lemma: rel_exp_add
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀m,n:ℕ. ∀[x,y,z:T]. ((x R^m y) ⇒ (y R^n z) ⇒ (x R^m + n z))
Lemma: rel_exp_add_iff
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀m,n:ℕ. ∀x,z:T. (x R^m + n z ⇐⇒ ∃y:T. ((x R^m y) ∧ (y R^n z)))
Lemma: rel_exp_add-ext
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀m,n:ℕ. ∀[x,y,z:T]. ((x R^m y) ⇒ (y R^n z) ⇒ (x R^m + n z))
Lemma: rel_exp1
∀[T:Type]. ∀[R:T ⟶ T ⟶ Type]. ∀[x:T]. ∀y:T. (R^1 x y ⇐⇒ R x y)
Definition: rel_implies
R1 => R2 == ∀x,y:T. ((x R1 y) ⇒ (x R2 y))
Lemma: rel_implies_wf
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 => R2 ∈ ℙ)
Lemma: rel_exp_monotone
∀n:ℕ. ∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 => R2 ⇒ R1^n => R2^n)
Definition: preserved_by
R preserves P == ∀x,y:T. ((P x) ⇒ (x R y) ⇒ (P y))
Lemma: preserved_by_wf
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ ℙ]. (R preserves P ∈ ℙ)
Lemma: preserved_by_monotone
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. ((∀x,y:T. ((x R1 y) ⇒ (x R2 y))) ⇒ R2 preserves P ⇒ R1 preserves P)
Definition: cond_rel_implies
when P, R1 => R2 == ∀x,y:T. ((P x) ⇒ (x R1 y) ⇒ (x R2 y))
Lemma: cond_rel_implies_wf
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (when P, R1 => R2 ∈ ℙ)
Lemma: cond_rel_exp_monotone
∀n:ℕ. ∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (when P, R1 => R2 ⇒ R1 preserves P ⇒ when P, R1^n => R2^n)
Definition: rel_star
R^* == λx,y. ∃n:ℕ. (x R^n y)
Lemma: rel_star_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (R^* ∈ T ⟶ T ⟶ ℙ)
Lemma: rel_star_monotone
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 => R2 ⇒ R1^* => R2^*)
Lemma: cond_rel_star_monotone
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (when P, R1 => R2 ⇒ R1 preserves P ⇒ when P, R1^* => R2^*)
Lemma: rel_star_transitivity
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[x,y,z:T]. ((x (R^*) y) ⇒ (y (R^*) z) ⇒ (x (R^*) z))
Lemma: rel_star_transitivity_ext
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[x,y,z:T]. ((x (R^*) y) ⇒ (y (R^*) z) ⇒ (x (R^*) z))
Definition: rel-connected
x──R⟶y == x (R^*) y
Lemma: rel-connected_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[x,y:T]. (x──R⟶y ∈ ℙ)
Lemma: rel-connected_transitivity
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[x,y,z:T]. (x──R⟶y ⇒ y──R⟶z ⇒ x──R⟶z)
Lemma: rel-connected_weakening
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[x,y:T]. x──R⟶y supposing x = y ∈ T
Lemma: test-rel-connected
∀T:Type. ∀R:T ⟶ T ⟶ ℙ. ∀x,y,z,w:T. ((x (R^*) y) ⇒ (y = z ∈ T) ⇒ (z (R^*) w) ⇒ (x (R^*) w))
Lemma: rel_star_monotonic
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. ∀x,y:T. (R1 => R2 ⇒ (x (R1^*) y) ⇒ (x (R2^*) y))
Lemma: cond_rel_star_monotonic
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ].
(when P, R1 => R2 ⇒ R1 preserves P ⇒ (∀x,y:T. ((P x) ⇒ (x (R1^*) y) ⇒ (x (R2^*) y))))
Lemma: preserved_by_star
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ ℙ]. (R preserves P ⇒ R^* preserves P)
Lemma: rel_star_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) ∨ (x = y ∈ T)))))
Lemma: rel_star_closure2
∀[T:Type]. ∀[R,R2:T ⟶ T ⟶ ℙ].
(Refl(T)(R2[_1;_2]) ⇒ Trans(T)(R2[_1;_2]) ⇒ (∀x,y:T. ((x R y) ⇒ R2[x;y])) ⇒ (∀x,y:T. ((x (R^*) y) ⇒ R2[x;y])))
Lemma: rel_star_of_equiv
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀x,y:T. (EquivRel(T)(_1 E _2) ⇒ (x (E^*) y) ⇒ (x E y))
Lemma: cond_rel_star_equiv
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,E:T ⟶ T ⟶ ℙ].
(EquivRel(T)(_1 E _2) ⇒ when P, R1 => E ⇒ R1 preserves P ⇒ when P, R1^* => E)
Lemma: rel_rel_star
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀x,y:T. ((x R y) ⇒ (x (R^*) y))
Lemma: rel_star_trans
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀x,y,z:T. ((x R y) ⇒ (y (R^*) z) ⇒ (x (R^*) z))
Lemma: rel_star_weakening
∀[T:Type]. ∀[x,y:T]. ∀[R:T ⟶ T ⟶ ℙ]. x (R^*) y supposing x = y ∈ T
Definition: rel_inverse
R^-1 == λx,y. (y R x)
Lemma: rel_inverse_wf
∀[T1,T2:Type]. ∀[R:T1 ⟶ T2 ⟶ ℙ]. (R^-1 ∈ T2 ⟶ T1 ⟶ ℙ)
Lemma: rel_inverse_exp
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀n:ℕ. ∀x,y:T. (x R^n^-1 y ⇐⇒ x R^-1^n y)
Lemma: rel_inverse_star
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀x,y:T. (x R^*^-1 y ⇐⇒ x (R^-1^*) y)
Lemma: rel_star_symmetric
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. (Sym(T;x,y.x R y) ⇒ Sym(T;x,y.x (R^*) y))
Lemma: rel_star_symmetric_2
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀x,y:T. (Sym(T;x,y.x R y) ⇒ (x (R^*) y) ⇒ (y (R^*) x))
Lemma: preserved_by_symmetric
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ ℙ]. (Sym(T;x,y.x R y) ⇒ R preserves P ⇒ R^-1 preserves P)
Definition: rel_or
R1 ∨ R2 == λx,y. ((x R1 y) ∨ (x R2 y))
Lemma: rel_or_wf
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 ∨ R2 ∈ T ⟶ T ⟶ ℙ)
Lemma: rel_implies_or_left
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. R1 => R1 ∨ R2
Lemma: rel_implies_or_right
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. R2 => R1 ∨ R2
Lemma: symmetric_rel_or
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (Sym(T;x,y.x R1 y) ⇒ Sym(T;x,y.x R2 y) ⇒ Sym(T;x,y.x (R1 ∨ R2) y))
Lemma: preserved_by_or
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 preserves P ⇒ R2 preserves P ⇒ R1 ∨ R2 preserves P)
Definition: rel_equivalent
R1 ⇐⇒ R2 == ∀x,y:T. (R1 x y ⇐⇒ R2 x y)
Lemma: rel_equivalent_wf
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 ⇐⇒ R2 ∈ ℙ)
Lemma: rel_equivalent_weakening
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. R1 ⇐⇒ R2 supposing R1 = R2 ∈ (T ⟶ T ⟶ ℙ)
Lemma: rel_implies_weakening
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 ⇐⇒ R2 ⇒ R1 => R2)
Lemma: rel_implies_transitivity
∀[T:Type]. ∀[R1,R2,R3:T ⟶ T ⟶ ℙ]. (R1 => R2 ⇒ R2 => R3 ⇒ R1 => R3)
Lemma: rel_equivalent_transitivity
∀[T:Type]. ∀[R1,R2,R3:T ⟶ T ⟶ ℙ]. (R1 ⇐⇒ R2 ⇒ R2 ⇐⇒ R3 ⇒ R1 ⇐⇒ R3)
Lemma: rel_equivalent_inversion
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 ⇐⇒ R2 ⇒ R2 ⇐⇒ R1)
Definition: rel_rev_implies
R1 ⇐ R2 == R2 => R1
Lemma: rel_rev_implies_wf
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 ⇐ R2 ∈ ℙ)
Lemma: rel_rev_implies_weakening
∀[T:Type]. ∀[R1,R2:T ⟶ T ⟶ ℙ]. (R1 ⇐⇒ R2 ⇒ R1 ⇐ R2)
Lemma: rel_implies_functionality
∀[T:Type]. ∀[A1,A2,B1,B2:T ⟶ T ⟶ ℙ]. (A1 ⇐ A2 ⇒ B1 => B2 ⇒ {A1 => B1 ⇒ A2 => B2})
Definition: rel-comp
(R1 o R2) == λx,z. ∃y:B. ((R1 x y) ∧ (R2 y z))
Lemma: rel-comp_wf
∀[A,B,C:Type]. ∀[R1:A ⟶ B ⟶ ℙ]. ∀[R2:B ⟶ C ⟶ ℙ]. ((R1 o R2) ∈ A ⟶ C ⟶ ℙ)
Lemma: rel-comp-exp
∀[T:Type]. ∀[R,S:T ⟶ T ⟶ ℙ]. ∀n:ℕ. (R o S)^n ⇐⇒ if (n =z 0) then λx,y. (x = y ∈ T) else (R o ((S o R)^n - 1 o S)) fi\000C
Lemma: rel-comp-star
∀[T:Type]. ∀[R,S:T ⟶ T ⟶ ℙ]. (R o S)^* ⇐⇒ (R o ((S o R)^* o S)) ∨ (λx,y. (x = y ∈ T))
Definition: isect-rel
⋂i:T. R[i] == λx,y. ∀i:T. (R[i] x y)
Lemma: isect-rel_wf
∀[T,A:Type]. ∀[R:T ⟶ A ⟶ A ⟶ ℙ]. (⋂i:T. R[i] ∈ A ⟶ A ⟶ ℙ)
Definition: rel-monotone
rel-monotone{i:l}(T;R.F[R]) == ∀R1,R2:T ⟶ T ⟶ ℙ. (R1 => R2 ⇒ F[R1] => F[R2])
Lemma: rel-monotone_wf
∀[T:Type]. ∀[F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ]. (rel-monotone{i:l}(T;R.F[R]) ∈ ℙ')
Definition: rel-continuous
rel-continuous{i:l}(T;R.F[R]) == ∀R:ℕ ⟶ T ⟶ T ⟶ ℙ. ⋂n:ℕ. F[R n] => F[⋂n:ℕ. R n]
Lemma: rel-continuous_wf
∀[T:Type]. ∀[F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ]. (rel-continuous{i:l}(T;R.F[R]) ∈ ℙ')
Definition: bigrel
If for R a relation on T (i.e. a member of type T ⟶ T ⟶ ℙ)
F(R) is another relation on T, then νR.F[R] is meant to be the
greatest relation on T that is a fixed point of F.
If F has the properties
rel-monotone{i:l}(T;R.F[R]) and
rel-continuous{i:l}(T;R.F[R])
then this will be so
(see bigrel-iff) ⋅
νR.F[R] == ⋂n:ℕ. primrec(n;λx,y. True;λm,R. F[R])
Lemma: bigrel_wf
∀[T:𝕌']. ∀[F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ]. (νR.F[R] ∈ T ⟶ T ⟶ ℙ)
Lemma: bigrel-iff
∀[T:Type]
∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ
(rel-monotone{i:l}(T;R.F[R]) ⇒ rel-continuous{i:l}(T;R.F[R]) ⇒ (νR.F[R] => F[νR.F[R]] ∧ F[νR.F[R]] => νR.F[R]))
Lemma: bigrel-induction
∀[T:Type]
∀P:(T ⟶ T ⟶ ℙ) ⟶ ℙ. ∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ.
((∀Rs:ℕ ⟶ T ⟶ T ⟶ ℙ. ((∀n:ℕ. P[Rs[n]]) ⇒ P[⋂n:ℕ. Rs[n]]))
⇒ (∀R:T ⟶ T ⟶ ℙ. (P[R] ⇒ P[F[R]]))
⇒ P[λx,y. True]
⇒ P[νR.F[R]])
Lemma: bigrel-induction-monotone
∀[T:Type]
∀P:(T ⟶ T ⟶ ℙ) ⟶ ℙ. ∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ.
(rel-monotone{i:l}(T;R.F[R])
⇒ (∀Rs:ℕ ⟶ T ⟶ T ⟶ ℙ. ((∀n:ℕ. Rs[n + 1] => Rs[n]) ⇒ (∀n:ℕ. P[Rs[n]]) ⇒ P[⋂n:ℕ. Rs[n]]))
⇒ (∀R:T ⟶ T ⟶ ℙ. (P[R] ⇒ P[F[R]]))
⇒ P[λx,y. True]
⇒ P[νR.F[R]])
Lemma: implies-bigrel
∀[T:Type]
∀F:(T ⟶ T ⟶ ℙ) ⟶ T ⟶ T ⟶ ℙ. (rel-monotone{i:l}(T;R.F[R]) ⇒ (∀R':T ⟶ T ⟶ ℙ. (R' => F[R'] ⇒ R' => νR.F[R])))
Definition: as_strong
P as strong as Q == ∀x:T. ((P x) ⇒ (Q x))
Lemma: as_strong_wf
∀[T:Type]. ∀[Q,P:T ⟶ ℙ]. (P as strong as Q ∈ ℙ)
Lemma: as_strong_transitivity
∀[T:Type]. ∀[P,Q,R:T ⟶ ℙ]. (P as strong as Q ⇒ Q as strong as R ⇒ P as strong as R )
Definition: prop_and
P ∧ Q == λL.((P L) ∧ (Q L))
Lemma: prop_and_wf
∀[T:Type]. ∀[P,Q:T ⟶ ℙ]. (P ∧ Q ∈ T ⟶ ℙ)
Lemma: and_preserved_by
∀[T:Type]. ∀[P,Q:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ ℙ]. (R preserves P ⇒ R preserves Q ⇒ R preserves P ∧ Q)
Definition: preserved_by2
(ternary) R preserves P == ∀x,y,z:T. ((P x) ⇒ (P y) ⇒ (R x y z) ⇒ (P z))
Lemma: preserved_by2_wf
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ T ⟶ ℙ]. ((ternary) R preserves P ∈ ℙ)
Lemma: and_preserved_by2
∀[T:Type]. ∀[P,Q:T ⟶ ℙ]. ∀[R:T ⟶ T ⟶ T ⟶ ℙ].
((ternary) R preserves P ⇒ (ternary) R preserves Q ⇒ (ternary) R preserves P ∧ Q )
Definition: predicate_or
P1 ∨ P2 == λx.((P1 x) ∨ (P2 x))
Lemma: predicate_or_wf
∀[T:Type]. ∀[P1,P2:T ⟶ ℙ]. (P1 ∨ P2 ∈ T ⟶ ℙ)
Definition: predicate_implies
P1 ⇒ P2 == ∀x:T. ((P1 x) ⇒ (P2 x))
Lemma: predicate_implies_wf
∀[T:Type]. ∀[P1,P2:T ⟶ ℙ]. (P1 ⇒ P2 ∈ ℙ)
Definition: predicate_rev_implies
P1 ⇐ P2 == P2 ⇒ P1
Lemma: predicate_rev_implies_wf
∀[T:Type]. ∀[P1,P2:T ⟶ ℙ]. (P1 ⇐ P2 ∈ ℙ)
Definition: predicate_equivalent
P1 ⇐⇒ P2 == ∀x:T. (P1 x ⇐⇒ P2 x)
Lemma: predicate_equivalent_wf
∀[T:Type]. ∀[P1,P2:T ⟶ ℙ]. (P1 ⇐⇒ P2 ∈ ℙ)
Lemma: predicate_equivalent_implies
∀[T:Type]. ∀[P1,P2:T ⟶ Type]. (P1 ⇐⇒ P2 ⇐⇒ P1 ⇒ P2 ∧ P2 ⇒ P1)
Lemma: predicate_implies_weakening
∀[T:Type]. ∀[P1,P2:T ⟶ ℙ]. (P1 ⇐⇒ P2 ⇒ P1 ⇒ P2)
Lemma: predicate_rev_implies_weakening
∀[T:Type]. ∀[P1,P2:T ⟶ ℙ]. (P1 ⇐⇒ P2 ⇒ P1 ⇐ P2)
Lemma: predicate_equivalent_weakening
∀[T:Type]. ∀[P1,P2:T ⟶ ℙ]. P1 ⇐⇒ P2 supposing P1 = P2 ∈ (T ⟶ ℙ)
Lemma: predicate_implies_reflexivity
∀[T:Type]. ∀[P:T ⟶ ℙ]. P ⇒ P
Lemma: predicate_implies_transitivity
∀[T:Type]. ∀[P1,P2,P3:T ⟶ ℙ]. (P1 ⇒ P2 ⇒ P2 ⇒ P3 ⇒ P1 ⇒ P3)
Lemma: predicate_equivalent_transitivity
∀[T:Type]. ∀[P1,P2,P3:T ⟶ ℙ]. (P1 ⇐⇒ P2 ⇒ P2 ⇐⇒ P3 ⇒ P1 ⇐⇒ P3)
Lemma: predicate_equivalent_inversion
∀[T:Type]. ∀[P1,P2:T ⟶ ℙ]. (P1 ⇐⇒ P2 ⇒ P2 ⇐⇒ P1)
Lemma: predicate_or_idempotent
∀[T:Type]. ∀[P:T ⟶ ℙ]. P ∨ P ⇐⇒ P
Definition: rel-restriction
R|P == λx,y. (((R x y) ∧ (P x)) ∧ (P y))
Lemma: rel-restriction_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ]. (R|P ∈ T ⟶ T ⟶ ℙ)
Lemma: rel-restriction-implies
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ]. R|P => R
Lemma: restriction-of-transitive
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ]. (Trans(T;x,y.R x y) ⇒ Trans(T;x,y.R|P x y))
Lemma: restriction-to-field
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ]. ((∀x,y:T. ((R x y) ⇒ ((P x) ∧ (P y)))) ⇒ (∀x,y:T. (R|P x y ⇐⇒ R x y)))
Definition: subsequence
subsequence(a,b.E[a; b];m.x[m];n.y[n]) == ∃N:ℕ. ∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ E[y[n]; x[m]]) supposing N ≤ n
Lemma: subsequence_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀[x,y:ℕ ⟶ T]. (subsequence(a,b.E[a;b];n.x[n];n.y[n]) ∈ ℙ)
Home
Index