theorem-prover/milawa-prover/milawa_logicScript.sml

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]]];