Lines Matching defs:i1
101 fun i1 q = GEN_ALL (Q.INST [`f` |-> q] prf1)
313 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`] THEN
315 SRW_TAC [][i1 `nfst`, prDIV, i2 `$+`, i1 `nsnd`],
621 val prmxabs = SIMP_RULE (srw_ss()) [] (i1 `max_abs o numdB`)
967 intro prCn3 THEN SRW_TAC [][i1 `nfst`, i1 `nsnd`] THEN
971 SRW_TAC [][combinTheory.o_ABS_R, prpred, pr_eq, i1`nsnd`, i2 `$+`] THENL [
972 intro primrec_FUNPOW THEN SRW_TAC [][i1 `nfst`] THEN
977 i2 `$+`, prpred, i1 `nsnd`]
985 SRW_TAC [][i2 `$-`, i2 `MAX`, prmxabs, i1 `nsnd`]
995 SRW_TAC [][i1 `nsnd`, prmxabs, i2 `$*`, i2 `$+`]