Lines Matching refs:i2
62 (\((s1, i1),(s2, i2)). (s1, i1, s2, i2) IN A.R /\ i1 SUBSET A.I /\ i2 SUBSET A.I)
262 !(S1 :'a set) (S2 :'a set) (i1 :'a set) (i2 :'a set).
264 (IS_TRANSITION A' S1 i1 S2 i2 <=>
265 (S2 = {s2 | s2 IN A'.S /\ ?s1. s1 IN S1 /\ IS_TRANSITION A (g s1) i1 (g s2) i2})))`;
354 INPUT_RUN_STATE_UNION A' i2 S2 DIFF A.S UNION l'') =
355 XP_SEM A.R (INPUT_RUN_STATE_UNION A i1 l', INPUT_RUN_STATE_UNION A i2 l'')` THEN1 (
361 ((INPUT_RUN_STATE_UNION A' i2 S2 DIFF A.S UNION l'') INTER XP_USED_X_VARS A.R =
362 (INPUT_RUN_STATE_UNION A i2 l'') INTER XP_USED_X_VARS A.R)` THEN1 (
506 IS_TRANSITION A (g s1') i1' (g s2) i2}` by PROVE_TAC[] THEN
1812 (!S1 S2 i1 i2.
1814 (IS_TRANSITION A' S1 i1 S2 i2 <=>
1817 IS_TRANSITION A (g s1) i1 (g s2) i2} UNION
1822 IS_TRANSITION A (g s1) i1 (g s2) i2 /\ (g s2) IN S}))))`;
2242 IS_TRANSITION A (g s1') (i1 UNION s1) (g s2) i2} UNION
2251 IS_TRANSITION A (g s1') (i1 UNION s1) (g s2) i2 /\
2473 (i2 DIFF
2488 SUBGOAL_TAC `!i1 i2 l' l''. XP_SEM A.R
2494 (i2 DIFF
2498 (XP_SEM A.R (l'' UNION (i1 DIFF A.S), l' UNION (i2 DIFF A.S)))` THEN1 (
2508 SUBGOAL_TAC `!i2 l'. (P_SEM
2510 (i2 DIFF