Step
*
1
2
of Lemma
cond_rel_star_equiv
1. [T] : Type
2. [P] : T ⟶ ℙ
3. [R1] : T ⟶ T ⟶ ℙ
4. [E] : T ⟶ T ⟶ ℙ
5. EquivRel(T)(_1 E _2)
6. when P, R1 => E
7. R1 preserves P
8. when P, R1^* => E^*
⊢ when P, R1^* => E
BY
{ (RepeatFor 5 (ParallelOp (-1))) }
1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. [R1] : T ⟶ T ⟶ ℙ
4. [E] : T ⟶ T ⟶ ℙ
5. EquivRel(T)(_1 E _2)
6. when P, R1 => E
7. R1 preserves P
8. ∀x,y:T. ((P x)
⇒ (x (R1^*) y)
⇒ (x (E^*) y))
9. x : T
10. ∀y:T. ((P x)
⇒ (x (R1^*) y)
⇒ (x (E^*) y))
11. y : T
12. P x
13. x (R1^*) y
14. x (E^*) y
⊢ x E y
Latex:
Latex:
1. [T] : Type
2. [P] : T {}\mrightarrow{} \mBbbP{}
3. [R1] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
4. [E] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
5. EquivRel(T)($_{1}$ E $_{2}$)
6. when P, R1 => E
7. R1 preserves P
8. when P, rel\_star(T; R1) => rel\_star(T; E)
\mvdash{} when P, rel\_star(T; R1) => E
By
Latex:
(RepeatFor 5 (ParallelOp (-1)))
Home
Index