Lines Matching defs:i0
69 ``!A i0 s0 p psl psl' sv. (sv =
71 (2 :num) * (2 :num) ** (SUC s0 - i0) + s0 + (3 :num) + n)) ==>
72 (i0 <= s0) ==>
73 (A.S = (INTERVAL_SET (SUC i0) s0)) ==>
78 (F_USED_VARS psl' SUBSET (INTERVAL_SET 0 i0)) ==>
90 (SUC (SUC s0) + 2 ** SUC (s0 - i0))
91 (SUC (SUC s0) + 2 ** SUC (s0 - i0) +
92 PRE (2 ** SUC (s0 - i0))))))))), PSL_TO_LTL psl')) l' ==>
95 DS.IV SUBSET INTERVAL_SET 0 (2 * 2**(SUC s0 - i0) + s0 + 2) ==>
98 (P_FORALL (INTERVAL_LIST (SUC i0) (SUC s0))
102 (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0))
103 (SUC i0))),
108 (INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0))
109 (PRE (2 ** SUC (s0 - i0)) +
110 (SUC (SUC s0) + 2 ** SUC (s0 - i0)))))),
117 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0))
121 (INTERVAL_LIST (SUC i0) (SUC s0)) (SUC (SUC s0))
122 (SUC i0)),
123 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0))
132 (INTERVAL_LIST (SUC i0) (SUC s0))
133 (SUC (SUC s0)) (SUC i0))))))),
135 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) (SUC s0))
141 n + 2 ** SUC (s0 - i0)
145 (INTERVAL_LIST (SUC i0) (SUC s0))
146 (SUC (SUC s0)) (SUC i0))),
147 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) (SUC s0))
161 2 ** SUC (s0 - i0))
162 (PRE (2 ** SUC (s0 - i0)) +
164 2 ** SUC (s0 - i0))))),
169 n + 2 ** SUC (s0 - i0)
173 (INTERVAL_LIST (SUC i0)
175 (SUC i0))),
178 (INTERVAL_LIST (SUC i0) (SUC s0))
179 (SUC (SUC s0)) (SUC i0))))))))),
193 Q_TAC EXISTS_TAC `i0` THEN
202 UNDISCH_NO_TAC 12 (*i0 <= s0*) THEN
221 ``!A i0 s0 p psl psl' sv.
223 (sv = \n:num. 2**(s0 - i0) + s0 + 1 + n) ==>
224 (i0 <= s0) ==>
225 (A.S = (INTERVAL_SET (SUC i0) s0)) ==>
230 (F_USED_VARS psl' SUBSET (INTERVAL_SET 0 i0)) ==>
236 (P_FORALL (INTERVAL_LIST (SUC i0) s0)
239 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0),
243 DS.IV SUBSET INTERVAL_SET 0 (2**(s0 - i0) + s0) ==>
247 (P_FORALL (INTERVAL_LIST (SUC i0) s0)
251 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0))),
255 (XP_NEXT_FORALL (INTERVAL_LIST (SUC i0) s0)
259 (INTERVAL_LIST (SUC i0) s0) (SUC s0) (SUC i0)),
260 XP_CURRENT_EXISTS (INTERVAL_LIST (SUC i0) s0)
265 (INTERVAL_LIST (SUC i0) s0) (SUC s0)
266 (SUC i0)))))),
283 Q_TAC EXISTS_TAC `i0` THEN
292 UNDISCH_NO_TAC 12 (*i0 <= s0*) THEN
339 val i0 = term_of_int ((int_of_term suc_i0) - 1);
342 val i0_le_s0_term = ``(i0:num) <= (s0:num)``;
344 mk_var ("i0", num) |-> i0,
348 val state_vars_term = ``(A:num symbolic_semi_automaton).S = INTERVAL_SET (SUC i0) s0``;
351 mk_var ("i0", num) |-> i0,
364 (s0, i0, i0_le_s0, state_vars, used_vars)
483 fun prepare_psl psl i0 =
499 val used_vars_term = ``F_USED_VARS psl SUBSET INTERVAL_SET 0 i0``;
502 mk_var ("i0", num) |-> i0] used_vars_term;
619 val (s0, i0, i0_le_s0, state_vars, semi_automaton_used_vars) =
621 val (psl', equiv_thm, cs_free_thm, psl_used_vars, psl_to_ltl) = prepare_psl psl i0
623 val thm = ISPECL [A, i0, s0, p, psl, psl'] thm;
660 val i_term = ``INTERVAL_LIST (SUC i0) (SUC s0)``
662 mk_var ("i0", num) |-> i0,
667 val i_term = ``(INTERVAL_LIST (SUC (SUC s0) + 2 ** SUC (s0 - i0))
668 (PRE (2 ** SUC (s0 - i0)) +
669 (SUC (SUC s0) + 2 ** SUC (s0 - i0))))``;
671 mk_var ("i0", num) |-> i0,
678 (INTERVAL_LIST (SUC i0) (SUC s0))
679 (SUC (SUC s0)) (SUC i0)``;
681 mk_var ("i0", num) |-> i0,
716 val (s0, i0, i0_le_s0, state_vars, semi_automaton_used_vars) =
718 val (psl', equiv_thm, cs_free_thm, psl_used_vars, psl_to_ltl) = prepare_psl psl i0
720 val thm = ISPECL [A, i0, s0, p, psl, psl'] thm;
779 val i_term = ``INTERVAL_LIST (SUC i0) s0``
781 mk_var ("i0", num) |-> i0,
787 (INTERVAL_LIST (SUC i0) s0)
788 (SUC s0) (SUC i0)``;
790 mk_var ("i0", num) |-> i0,