Lines Matching defs:implies
94 (defthm rcdp-implies-true-listp
95 (implies (rcdp x)
105 (implies (and (rcdp r)
113 (implies (rcdp r)
118 (implies (rcdp r)
124 (implies (and (rcdp r)
131 (implies (rcdp r)
137 (implies (rcdp r)
143 (implies (and (rcdp r)
151 (implies (and v (rcdp r))
156 (implies (and (rcdp r)
162 (implies (rcdp r)
168 (implies (rcdp r)
176 (implies (rcdp r)
184 (implies (rcdp x)
203 (implies (and r (rcdp r))
216 (implies (not (equal a b))
240 (implies (not (equal a b))
262 (implies v (s a v r))
269 (implies (g a r) r)
274 (implies (equal v (g a r))