Skip to main content

axiom/NatPow

Reference for mo:core/axiom/NatPow 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/NatPow

Status​

  • Spec-only axiom module

Public API​

Types​

  • Nat

Lemmas​

powZeroExp(a : Nat) : ()​

Establishes Nat.pow(a, 0) == 1 in the current proof context.

Contract

ensures Nat.pow(a, 0) == 1;

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

powStep(a : Nat, n : Nat) : ()​

Establishes Nat.pow(a, n + 1) == Nat.pow(a, n) * a in the current proof context.

Contract

ensures Nat.pow(a, n + 1) == Nat.pow(a, n) * a;

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

powOneBase(n : Nat) : ()​

Establishes Nat.pow(1, n) == 1 in the current proof context.

Contract

ensures Nat.pow(1, n) == 1;

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

powZeroBase(n : Nat) : ()​

Establishes Nat.pow(0, n + 1) == 0 in the current proof context.

Contract

ensures Nat.pow(0, n + 1) == 0;

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

powMonoExp(a : Nat, n : Nat, m : Nat) : ()​

Establishes Nat.pow(a, n) <= Nat.pow(a, m) in the current proof context.

Contract

requires a >= 2;
requires n <= m;
ensures Nat.pow(a, n) <= Nat.pow(a, m);

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

powPos(a : Nat, n : Nat) : ()​

Establishes Nat.pow(a, n) > 0 in the current proof context.

Contract

requires a > 0;
ensures Nat.pow(a, n) > 0;

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

powAddExp(a : Nat, n : Nat, m : Nat) : ()​

Establishes Nat.pow(a, n + m) == Nat.pow(a, n) * Nat.pow(a, m) in the current proof context.

Contract

ensures Nat.pow(a, n + m) == Nat.pow(a, n) * Nat.pow(a, m);

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

powGrowth(a : Nat, n : Nat) : ()​

Establishes Nat.pow(a, n) >= a in the current proof context.

Contract

requires a >= 2;
requires n > 0;
ensures Nat.pow(a, n) >= 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/NatPow.
  • Exposes 8 trusted lemmas.