Lines Matching defs:less
232 val less = ``mApp (mPrimitiveFun logic_LESS)``
353 (^por (^pequal (^less [^x;^y]) ^nnil)
354 (^pequal (^less [^x;^y]) ^t));
356 (^pequal (^less [^a;^a]) ^nnil);
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])));
362 (* Axiom 36. less-completion-left *)
364 (^pequal (^less [^a;^b]) (^less [^zero;^b])));
365 (* Axiom 37. less-completion-right *)
367 (^pequal (^less [^a;^b]) ^nnil));
369 (^por (^pequal (^less [^a;^b]) ^nnil)
370 (^por (^pequal (^less [^b;^c]) ^nnil)
371 (^pequal (^less [^a;^c]) ^t)));
375 (^por (^pequal (^less [^a;^b]) ^t)
376 (^por (^pequal (^less [^b;^a]) ^t)
379 (^por (^pequal (^less [^a;^b]) ^nnil)
380 (^pequal (^less [^b;^add [^one;^a]]) ^nnil));
381 (* Axiom 41. natural-less-than-one-is-zero *)
383 (^por (^pequal (^less [^a;^one]) ^nnil)
385 (* Axiom 42. less-than-of-plus-and-plus *)
386 (^pequal (^less [^add [^a;^b];^add [^a;^c]]) (^less [^b;^c]));
390 (^por (^pequal (^less [^b;^a]) ^t)
395 (* Axiom 46. less-of-minus-left *)
396 (^por (^pequal (^less [^b;^a]) ^nnil)
397 (^pequal (^less [^sub [^a;^b];^c])
398 (^less [^a;^add [^b;^c]])));
399 (* Axiom 47. less-of-minus-right *)
400 (^pequal (^less [^a;^sub [^b;^c]])
401 (^less [^add [^a;^c];^b]));
403 (^por (^pequal (^less [^c;^b]) ^nnil)
407 (^por (^pequal (^less [^c;^b]) ^nnil)
414 (^por (^pequal (^less [^b;^a]) ^nnil)
431 ^iff [^consp [^y]; ^t; (^less [^x;^y])];
437 ^less [^cdr [^car [^x]]; ^cdr [^car [^y]]];
446 (^iff [^less [^zero; ^cdr [^car [^x]]];