Lines Matching defs:i2
91 fun i2 q = GEN_ALL (Q.INST [`f` |-> q] prf2)
93 fun intro2 q = HO_MATCH_MP_TAC (i2 q)
301 SRW_TAC [][prCn2, i2 `ncons`] THEN
306 SRW_TAC [][prDIV, i2 `$+`],
313 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`] THEN
315 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`],
320 SRW_TAC [][i2 `nel`, i2 `$+`, prDIV],
322 SRW_TAC [][pr_eq, prMOD, i2 `$+`]
325 SRW_TAC [][pr_eq, prMOD, i2 `$+`]
418 SRW_TAC [][i2 `$*`, prK] THEN
632 SRW_TAC [][i2 `ncons`, i2 `$+`, i2 `$*`] THEN
634 SRW_TAC [][combinTheory.o_ABS_R, i2 `napp`, i2 `$*`, i2 `ncons`, prpred]
637 SRW_TAC [][i2 `ncons`, i2 `$+`, i2 `$*`],
638 SRW_TAC [][i2 `$+`]
645 SRW_TAC [][i2 `$+`, i2 `$*`, i2 `npair`, i2 `nel`],
650 SRW_TAC [][i2 `$+`, i2 `$*`, i2 `npair`, i2 `nel`]
658 SRW_TAC [][prmxabs, i2 `$-`, i2 `$+`] THEN
661 SRW_TAC [][i2 `nel`, i2 `$*`, i2 `$+`],
665 SRW_TAC [][i2 `nel`, i2 `$+`, i2 `$*`]
669 SRW_TAC [][prmxabs, i2 `$+`]
965 intro prCn2 THEN SRW_TAC [][i2 `npair`, prmxabs, i2 `$+`] THEN
971 SRW_TAC [][combinTheory.o_ABS_R, prpred, pr_eq, i1`nsnd`, i2 `$+`] THENL [
976 intro prCOND THEN SRW_TAC [][combinTheory.o_ABS_R, i2 `$*`, i2 `$-`,
977 i2 `$+`, prpred, i1 `nsnd`]
982 [alt_Pr_rule, i2 `napp`, i2 `ncons`] THEN
984 SRW_TAC [][i2 `$*`, i2 `nel`, i2 `npair`],
985 SRW_TAC [][i2 `$-`, i2 `MAX`, prmxabs, i1 `nsnd`]
990 [alt_Pr_rule, i2 `napp`, i2 `ncons`] THEN
992 SRW_TAC [][i2 `$*`, i2 `$+`, i2 `nel`],
995 SRW_TAC [][i1 `nsnd`, prmxabs, i2 `$*`, i2 `$+`]
1079 intro primrec_prtermrec0 THEN SRW_TAC [][i2 `$*`, i2 `$+`] THEN
1084 SRW_TAC [][prpred, combinTheory.o_ABS_R, i2 `$*`, i2 `npair`, i2 `$+`,