Lines Matching defs:i1
104 fun i1 q = GEN_ALL (Q.INST [`f` |-> q] prf1)
318 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`] THEN
320 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`],
628 val prmxabs = SIMP_RULE (srw_ss()) [] (i1 `max_abs o numdB`)
972 intro prCn3 THEN SRW_TAC [][i1 `nfst`, i1 `nsnd`] THEN
976 SRW_TAC [][combinTheory.o_ABS_R, prpred, pr_eq, i1`nsnd`, i2 `$+`] THENL [
977 intro primrec_FUNPOW THEN SRW_TAC [][i1 `nfst`] THEN
982 i2 `$+`, prpred, i1 `nsnd`]
990 SRW_TAC [][i2 `$-`, i2 `MAX`, prmxabs, i1 `nsnd`]
1000 SRW_TAC [][i1 `nsnd`, prmxabs, i2 `$*`, i2 `$+`]