Provedalphaalpha-core-v0evaluation

Alpha Core v0: the fixture evaluates to 1

\htmlData{mx=5}{\htmlData{mx=0}{\operatorname{Evaluates}}\,\htmlData{mx=1}{\operatorname{fixture}}\,\htmlData{mx=4}{\htmlData{mx=2}{\operatorname{successor}}(\htmlData{mx=3}{\operatorname{zero}})}}

What the notation means · or point at any symbol

Evaluates: Evaluates: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Evaluates)
fixture: fixture: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (fixture)
successor: Term.successor: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Term.successor)
f(x)Function application: Term.successor applied to zero. Lean writes f x; papers write f(x). (Term.successor Term.zero)
zero: Term.zero: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Term.zero)

theorem alpha-core-v0-fixture-evaluates :
    Evaluates fixture (Term.successor Term.zero)

Under Alpha Core v0's big-step evaluation the fixture (identity Nat) (successor zero) evaluates to successor zero.

How it was proved

Proved: 21 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 13 lines of Lean