axiom/IntOrder

Reference for mo:core/axiom/IntOrder in the core library.

This page lists trusted proof lemmas. Calling one adds its ensures facts after its requires clauses are proven; the lemma body itself is part of the trusted base, not a verifier-checked derivation. Use these when ordinary SMT arithmetic needs a precise algebraic step.

Import

mo:core/axiom/IntOrder

Status

• Spec-only axiom module

Public API

Types

• Int

Lemmas

leAntisym(a : Int, b : Int) : ()

Establishes a == b in the current proof context.

Contract

requires a <= b;
requires b <= a;
ensures a == b;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

leTrans(a : Int, b : Int, c : Int) : ()

Establishes a <= c in the current proof context.

Contract

requires a <= b;
requires b <= c;
ensures a <= c;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

leTotal(a : Int, b : Int) : ()

Establishes a <= b or b <= a in the current proof context.

Contract

ensures a <= b or b <= a;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

ltStep(a : Int, b : Int) : ()

Establishes (a < b) <==> (a + 1 <= b) in the current proof context.

Contract

ensures (a < b) <==> (a + 1 <= b);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

leCancelAdd(a : Int, b : Int, k : Int) : ()

Establishes (a + k <= b + k) <==> (a <= b) in the current proof context.

Contract

ensures (a + k <= b + k) <==> (a <= b);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

ltCancelAdd(a : Int, b : Int, k : Int) : ()

Establishes (a + k < b + k) <==> (a < b) in the current proof context.

Contract

ensures (a + k < b + k) <==> (a < b);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

leNegFlip(a : Int, b : Int) : ()

Establishes (a <= b) <==> (-b <= -a) in the current proof context.

Contract

ensures (a <= b) <==> (-b <= -a);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

Summary

• Spec-only axiom module under mo:core/axiom/IntOrder.
• Exposes 7 trusted lemmas.