Lines Matching refs:zero
255 val zero = ``mConst (Val 0)``
348 (^pequal (^add [^a;^b]) (^add [^zero;^b])));
349 (* Axiom 31. plus-of-zero-when-natural *)
351 (^pequal (^add [^a;^zero]) ^a));
357 (* Axiom 34. less-of-zero-right *)
358 (^pequal (^less [^a;^zero]) ^nnil);
359 (* Axiom 35. less-of-zero-left-when-natp *)
361 (^pequal (^less [^zero;^a]) (^iff [^eequal [^a;^zero];^nnil;^t])));
364 (^pequal (^less [^a;^b]) (^less [^zero;^b])));
381 (* Axiom 41. natural-less-than-one-is-zero *)
384 (^pequal ^a ^zero)));
391 (^pequal (^sub [^a;^b]) ^zero));
394 (^iff [^natp [^a];^a;^zero]));
427 ^zero]));
445 (^iff [^nnot [^eequal [^car [^car [^x]]; ^zero]];
446 (^iff [^less [^zero; ^cdr [^car [^x]]];