- change with (eq1 ? (b⎻* (a'⎻* (A o1 x))) (b'⎻*(a'⎻* (A o1 x))));
- apply (.= †(saturated o1 o2 a' (A o1 x) ?)); [
- apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
- apply (.= (e1 (a'⎻* (A o1 x))));
- change with (eq1 ? (b'⎻* (A o2 (a'⎻* (A o1 x)))) (b'⎻*(a'⎻* (A o1 x))));
- apply (.= †(saturated o1 o2 a' (A o1 x):?)^-1); [
- apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
+ change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x))));
+ apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
+ apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
+ apply (.= (e1 (a'⎻* (oA o1 x))));
+ change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));
+ apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
+ apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]