Lines Matching refs:i2
533 let (i2,t2,a2) = regexp2na r2 in
534 (i1 + i2 + 1,
536 if s <= i2 then t2 s x s'
537 else if s' <= i2 then a1 (s - (i2 + 1)) /\ t2 i2 x s'
538 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))),
539 \s. if s <= i2 then a2 s else a2 i2 /\ a1 (s - (i2 + 1)))) /\
542 let (i2,t2,a2) = regexp2na r2 in
543 (i1 + i2 + 1,
545 if s <= i2 then t2 s x s'
546 else if s' <= i2 then ?y. t1 (s - (i2 + 1)) x y /\ a1 y /\ t2 i2 x s'
547 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))),
551 let (i2,t2,a2) = regexp2na r2 in
552 (i1 + i2 + 2,
554 if s = i1 + i2 + 2 then
555 if s' <= i1 then t1 i1 x s' else t2 i2 x (s' - (i1 + 1))
559 if s = i1 + i2 + 2 then a1 i1 \/ a2 i2
563 let (i2,t2,a2) = regexp2na r2 in
564 (i1 * i2 + i1 + i2,
566 t1 (s DIV (i2 + 1)) x (s' DIV (i2 + 1)) /\
567 t2 (s MOD (i2 + 1)) x (s' MOD (i2 + 1))),
568 \s. a1 (s DIV (i2 + 1)) /\ a2 (s MOD (i2 + 1)))) /\
604 >> Introduce `regexp2na r2 = (i2,t2,a2)`
617 >> Introduce `regexp2na r2 = (i2,t2,a2)`
629 >> Introduce `regexp2na r2 = (i2,t2,a2)`
639 >> Introduce `regexp2na r2 = (i2,t2,a2)`
640 >> Q.PAT_X_ASSUM `!i. P i` (MP_TAC o Q.SPECL [`i2`,`t2`,`a2`])
647 >> MP_TAC (Q.SPEC `i2 + 1` DIVISION)
651 >> Q.EXISTS_TAC `(s DIV (i2 + 1)) * (i2 + 1) + i2`
661 >| [MP_TAC (Q.SPEC `i2 + 1` DIVISION)
665 >> Q.EXISTS_TAC `(s DIV (i2 + 1)) * (i2 + 1) + i2`
673 MP_TAC (Q.SPEC `i2 + 1` DIVISION)
677 >> Q.EXISTS_TAC `(s' DIV (i2 + 1)) * (i2 + 1) + i2`
729 >> Introduce `regexp2na r2 = (i2, t2, a2)`
736 (i1 + i2 + 1,
738 if s <= i2 then t2 s x s'
739 else if s' <= i2 then a1 (s - (i2 + 1)) /\ t2 i2 x s'
740 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))),
741 (\s. if s <= i2 then a2 s else a2 i2 /\ a1 (s - (i2 + 1))))
742 (k + i2 + 1) l =
745 na_step (i2,t2,a2) i2 w2`
765 ((?x : num. P (x + i2 + 1)) = Q) ==>
766 ((?x. ~(x <= i2) /\ P x) = Q)`
773 >> Suff `!x. ~(x <= i2) = (?y. x = y + i2 + 1)` >- METIS_TAC []
777 >> Q.EXISTS_TAC `x - (i2 + 1)`
800 >> Introduce `regexp2na r2 = (i2, t2, a2)`
806 (i1 + i2 + 1,
808 if s <= i2 then t2 s x s'
809 else if s' <= i2 then
810 ?y. t1 (s - (i2 + 1)) x y /\ a1 y /\ t2 i2 x s'
811 else t1 (s - (i2 + 1)) x (s' - (i2 + 1))),a2) (k + i2 + 1) l =
814 na_step (i2,t2,a2) i2 ([c] <> w2)`
818 >> Suff `~(k + i2 + 1 <= i2)` >- METIS_TAC [regexp2na_acc]
834 ((?x : num. P (x + i2 + 1)) = Q) ==>
835 ((?x. ~(x <= i2) /\ P x) = Q)`
843 >> Suff `!x. ~(x <= i2) = (?y. x = y + i2 + 1)` >- METIS_TAC []
847 >> Q.EXISTS_TAC `x - (i2 + 1)`
872 >> Introduce `regexp2na r2 = (i2, t2, a2)`
919 >> rename1 `na_step _ (i1 + (s'' + 1)) t = na_step (i2,t2,a2) s'' t`
920 >> Know `s'' <= i2` >- METIS_TAC [regexp2na_trans] (* was: s' *)
940 >> rename1 `na_step _ (i1 + (s'' + 1)) t = na_step (i2,t2,a2) s'' t`
942 >> Know `s'' <= i2` >- METIS_TAC [regexp2na_trans]
952 >> Introduce `regexp2na r2 = (i2, t2, a2)`
957 j <= i1 /\ k <= i2 ==>
959 (i1 * i2 + i1 + i2,
961 t1 (s DIV (i2 + 1)) x (s' DIV (i2 + 1)) /\
962 t2 (s MOD (i2 + 1)) x (s' MOD (i2 + 1))),
963 (\s. a1 (s DIV (i2 + 1)) /\ a2 (s MOD (i2 + 1))))
964 (j * (i2 + 1) + k) l =
965 na_step (i1,t1,a1) j l /\ na_step (i2,t2,a2) k l)`
966 >- (DISCH_THEN (MP_TAC o Q.SPECL [`i1`, `i2`])
968 >> Know `0 < i2 + 1` >- DECIDE_TAC >> STRIP_TAC
969 >> Know `!k. k < i2 + 1 = k <= i2` >- DECIDE_TAC >> STRIP_TAC
975 >> MP_TAC (Q.SPEC `i2 + 1` DIVISION)
987 >> Q.EXISTS_TAC `\x. x DIV (i2 + 1) <= i1 /\ x MOD (i2 + 1) <= i2`
999 >> rename1 `na_step (i2,t2,a2) s''' l`
1001 >> Q.EXISTS_TAC `s'' * (i2 + 1) + s'''` (* was: s', s'' *)
1002 >> Know `s''' <= i2` >- METIS_TAC [regexp2na_trans]
1252 let i2 = initial_regexp2na r2 in i1 * i2 + i1 + i2) /\
1258 >> Introduce `regexp2na r2 = (i2,t2,a2)`
1269 let i2 = initial_regexp2na r2 in
1270 if s <= i2 then accept_regexp2na r2 s
1271 else accept_regexp2na r2 i2 /\
1272 accept_regexp2na r1 (s - (i2 + 1))) /\
1276 let i2 = initial_regexp2na r2 in
1277 if s = i1 + i2 + 2 then
1278 accept_regexp2na r1 i1 \/ accept_regexp2na r2 i2
1282 let i2 = initial_regexp2na r2 in
1283 accept_regexp2na r1 (s DIV (i2 + 1)) /\
1284 accept_regexp2na r2 (s MOD (i2 + 1))) /\
1294 >> Introduce `regexp2na r2 = (i2,t2,a2)`
1339 let i2 = initial_regexp2na r2 in
1340 if s <= i2 then transition_regexp2na r2 s x s'
1341 else if s' <= i2 then
1342 accept_regexp2na r1 (s - (i2 + 1)) /\
1343 transition_regexp2na r2 i2 x s'
1345 transition_regexp2na r1 (s - (i2 + 1)) x (s' - (i2 + 1))) /\
1347 let i2 = initial_regexp2na r2 in
1348 if s <= i2 then transition_regexp2na r2 s x s'
1349 else if s' <= i2 then
1350 transition_regexp2na r2 i2 x s' /\
1353 (transition_regexp2na r1 (s - (i2 + 1)) x) (SUC i1)
1354 else transition_regexp2na r1 (s - (i2 + 1)) x (s' - (i2 + 1))) /\
1357 let i2 = initial_regexp2na r2 in
1358 if s = i1 + i2 + 2 then
1360 else transition_regexp2na r2 i2 x (s' - (i1 + 1))
1365 let i2 = initial_regexp2na r2 in
1366 transition_regexp2na r1 (s DIV (i2 + 1)) x (s' DIV (i2 + 1)) /\
1367 transition_regexp2na r2 (s MOD (i2 + 1)) x (s' MOD (i2 + 1))) /\
1379 >> Introduce `regexp2na r2 = (i2,t2,a2)`
1386 MP_TAC (Q.SPECL [`SUC i1`, `r1`, `s - (i2 + 1)`, `x`, `i1`, `t1`, `a1`]