constructor 1;
[ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
| intros;
- change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
+ change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
- with (c \sub \f ∘ c1 \sub \f);
+ with (c1 \sub \f ∘ c \sub \f);
change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
- with (c \sub \f ∘ c1 \sub \f);
+ with (c1 \sub \f ∘ c \sub \f);
apply (.= (extS_com ??????));
apply (.= (†(respects_converges ?????)));
apply (.= (respects_converges ?????));
apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
apply refl1;
- | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
+ | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c1 \sub \c ∘ c \sub \c);
apply (.= (extS_com ??????));
apply (.= (†(respects_all_covered ???)));
apply (.= respects_all_covered ???);
apply refl1]
| intros;
- change with (a ∘ b = a' ∘ b');
+ change with (b ∘ a = b' ∘ a');
change in H with (rp'' ?? a = rp'' ?? a');
change in H1 with (rp'' ?? b = rp ?? b');
apply (.= (H‡H1));
apply refl1]
| apply convergent_relation_space_composition
| intros; simplify;
- change with ((a12 ∘ a23) ∘ a34 = a12 ∘ (a23 ∘ a34));
+ change with (a34 ∘ (a23 ∘ a12) = (a34 ∘ a23) ∘ a12);
apply (.= ASSOC1);
apply refl1
| intros; simplify;
- change with (id1 ? o1 ∘ a = a);
- apply (.= id_neutral_left1 ????);
+ change with (a ∘ id1 ? o1 = a);
+ apply (.= id_neutral_right1 ????);
apply refl1
| intros; simplify;
- change with (a ∘ id1 ? o2 = a);
- apply (.= id_neutral_right1 ????);
+ change with (id1 ? o2 ∘ a = a);
+ apply (.= id_neutral_left1 ????);
apply refl1]
qed.