Lines Matching refs:f2
342 reachRelFromSet (ALTER_A f f0 f1 f2 f3) (BIGUNION f2)`
352 >> `���x. (oneStep (ALTER_A f f0 f1 f2 f3))^* x s ��� ���s. x ��� s ��� s ��� f2`
355 >- (`oneStep (ALTER_A f f0 f1 f2 f3) s s'` by (
392 >> rename [���reachRel (ALTER_A f f0 f1 f2 f3) b s���, ���b ��� s1���, ���s1 ��� f2���,
395 >- (`oneStep (ALTER_A f f0 f1 f2 f3) s x` by (
450 ��� q ��� reachRelFromSet (ALTER_A f f0 f1 f2 f3) (BIGUNION f2)`
479 (ALTER_A f f0 f1 f2 f3) (BIGUNION f2)}` by (
867 (* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *)
889 (* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *)
919 (* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *)
941 (* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *)
971 (* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *)
976 (* (replaceState x s_new f1) f2 (replaceBy f3 x s_new)).states` *)
1036 (* f1) f2 *)
1534 (* (@s. s ��� f ��� s ��� x ��� equivalentStates f1 f3 s x) f1) f2 *)