Lines Matching refs:g1
40 ; theorem (presumably proved by showing the existence of the g1 guaranteed by41 ; "some g1" below).42 ; Definition. g1 = some g1 . forall x . (integerp (g1 x))43 ; |- forall x . |= (integerp (g1 x))45 ((g1 (x) t))46 (local (defun g1 (x)49 (defthm integerp-g150 (integerp (g1 x))))