OP₀–OP₁₀ consistency and OP₁₁ extension

denP is den with evalPaper at * nodes. Also defines the OP₁₁ hint machine (nextHint/runHint) by expanding hints at reduction time.

OP₀–OP₁₀ denotation

def Nock.Verb.denP : ℕ → Verb → Option Noun

Like den, but * nodes use evalPaper (OP₀–OP₁₀; crashes on OP₁₁).

Equations

• One or more equations did not get rendered due to their size.
• Nock.Verb.denP x✝ (Nock.Verb.leaf k) = some (Nock.Noun.atom k)
• Nock.Verb.denP 0 (Nock.Verb.node a a_1 a_2) = none
• Nock.Verb.denP fuel.succ (Nock.Verb.node Nock.Action.null l r) = match Nock.Verb.denP fuel l, Nock.Verb.denP fuel r with | some a, some b => some (a.cell b) | x, x_1 => none
• Nock.Verb.denP fuel.succ (Nock.Verb.node Nock.Action.star l r) = match Nock.Verb.denP fuel l, Nock.Verb.denP fuel r with | some a, some b => Nock.evalPaper fuel a b | x, x_1 => none
• Nock.Verb.denP fuel.succ (Nock.Verb.node Nock.Action.equal l r) = match Nock.Verb.denP fuel l, Nock.Verb.denP fuel r with | some a, some b => some (a.tis b) | x, x_1 => none
• Nock.Verb.denP fuel.succ (Nock.Verb.node Nock.Action.edit l (Nock.Verb.leaf a)) = none
• Nock.Verb.denP fuel.succ (Nock.Verb.node Nock.Action.wut l r) = none

theorem Nock.Verb.denP_succ {n : ℕ} {v : Verb} {r : Noun} (h : denP n v = some r) : denP (n + 1) v = some r

theorem Nock.Verb.denP_mono {n m : ℕ} {v : Verb} {r : Noun} (hle : n ≤ m) (h : denP n v = some r) : denP m v = some r

theorem Nock.Verb.denP_terminal (v : Verb) (fuel : ℕ) : v.isTerminal = true → v.noun.size ≤ fuel → denP fuel v = some v.noun

denP of any terminal verb is its underlying noun (given adequate fuel). Identical to den_terminal: a terminal verb has no *-node, so evalPaper/evalN never enter.

theorem Nock.Verb.denP_ofNoun (n : Noun) (fuel : ℕ) : n.size ≤ fuel → denP fuel (ofNoun n) = some n

denP of the terminal verb ofNoun n is n (given adequate fuel; cf. den_ofNoun).

theorem Nock.Verb.denP_program (s f : Noun) (fuel : ℕ) (hs : s.size ≤ fuel) (hf : f.size ≤ fuel) : denP (fuel + 1) (program s f) = evalPaper fuel s f

denP of the initial program verb *[s, f] is evalPaper s f (cf. den_program).

theorem Nock.Verb.denP_iff_evalPaper (s f r : Noun) : (∃ (fuel : ℕ), denP fuel (program s f) = some r) ↔ ∃ (fuel : ℕ), evalPaper fuel s f = some r

denP ≡ evalPaper on program verbs, as partial functions (cf. den_iff_evalN).

def Nock.Verb.DenP (v : Verb) (x : Noun) : Prop

A verb has a paper-fragment denotation at some finite fuel.

Equations

• v.DenP x = ∃ (fuel : ℕ), Nock.Verb.denP fuel v = some x

def Nock.Verb.EvP (a b x : Noun) : Prop

Paper-fragment Nock evaluation succeeds with some finite fuel.

Equations

• Nock.Verb.EvP a b x = ∃ (fuel : ℕ), Nock.evalPaper fuel a b = some x

theorem Nock.Verb.denP_pair {l r : Verb} {a b : Noun} (hl : l.DenP a) (hr : r.DenP b) : ∃ (f : ℕ), denP f l = some a ∧ denP f r = some b

theorem Nock.Verb.denP_triple {a b c : Verb} {va vb vc : Noun} (ha : a.DenP va) (hb : b.DenP vb) (hc : c.DenP vc) : ∃ (f : ℕ), denP f a = some va ∧ denP f b = some vb ∧ denP f c = some vc

theorem Nock.Verb.denP_det {v : Verb} {r1 r2 : Noun} (h1 : v.DenP r1) (h2 : v.DenP r2) : r1 = r2

theorem Nock.Verb.ev2P {s1 f1 x1 s2 f2 x2 : Noun} (h1 : EvP s1 f1 x1) (h2 : EvP s2 f2 x2) : ∃ (f : ℕ), evalPaper f s1 f1 = some x1 ∧ evalPaper f s2 f2 = some x2

theorem Nock.Verb.ev3P {s1 f1 x1 s2 f2 x2 s3 f3 x3 : Noun} (h1 : EvP s1 f1 x1) (h2 : EvP s2 f2 x2) (h3 : EvP s3 f3 x3) : ∃ (f : ℕ), evalPaper f s1 f1 = some x1 ∧ evalPaper f s2 f2 = some x2 ∧ evalPaper f s3 f3 = some x3

EvP inversions (evalPaper analogues of the EvN_* family)

theorem Nock.Verb.EvP_autocons {subj hb hc d x : Noun} : EvP subj ((hb.cell hc).cell d) x ↔ ∃ (l : Noun) (r : Noun), x = l.cell r ∧ EvP subj (hb.cell hc) l ∧ EvP subj d r

theorem Nock.Verb.EvP_op0 {subj tail x : Noun} : EvP subj ((Noun.atom 0).cell tail) x ↔ ∃ (ax : ℕ), tail = Noun.atom ax ∧ Noun.slot ax subj = some x

theorem Nock.Verb.EvP_op1 {subj tail x : Noun} : EvP subj ((Noun.atom 1).cell tail) x ↔ x = tail

theorem Nock.Verb.EvP_op2 {subj tail x : Noun} : EvP subj ((Noun.atom 2).cell tail) x ↔ ∃ (hb : Noun) (hc : Noun) (sb : Noun) (sc : Noun), tail = hb.cell hc ∧ EvP subj hb sb ∧ EvP subj hc sc ∧ EvP sb sc x

theorem Nock.Verb.EvP_op3 {subj tail x : Noun} : EvP subj ((Noun.atom 3).cell tail) x ↔ ∃ (y : Noun), EvP subj tail y ∧ x = y.wut

theorem Nock.Verb.EvP_op4 {subj tail x : Noun} : EvP subj ((Noun.atom 4).cell tail) x ↔ ∃ (y : Noun), EvP subj tail y ∧ y.lus = some x

theorem Nock.Verb.EvP_op5 {subj tail x : Noun} : EvP subj ((Noun.atom 5).cell tail) x ↔ ∃ (hb : Noun) (hc : Noun) (sb : Noun) (sc : Noun), tail = hb.cell hc ∧ EvP subj hb sb ∧ EvP subj hc sc ∧ x = sb.tis sc

theorem Nock.Verb.EvP_op6 {subj tail x : Noun} : EvP subj ((Noun.atom 6).cell tail) x ↔ ∃ (b : Noun) (c : Noun) (d : Noun) (cv : Noun), tail = b.cell (c.cell d) ∧ EvP subj b cv ∧ (cv = Noun.atom 0 ∧ EvP subj c x ∨ cv = Noun.atom 1 ∧ EvP subj d x)

theorem Nock.Verb.EvP_op7 {subj tail x : Noun} : EvP subj ((Noun.atom 7).cell tail) x ↔ ∃ (hb : Noun) (hc : Noun) (sb : Noun), tail = hb.cell hc ∧ EvP subj hb sb ∧ EvP sb hc x

theorem Nock.Verb.EvP_op8 {subj tail x : Noun} : EvP subj ((Noun.atom 8).cell tail) x ↔ ∃ (hb : Noun) (hc : Noun) (sb : Noun), tail = hb.cell hc ∧ EvP subj hb sb ∧ EvP (sb.cell subj) hc x

theorem Nock.Verb.EvP_op9 {subj tail x : Noun} : EvP subj ((Noun.atom 9).cell tail) x ↔ ∃ (ax : ℕ) (c : Noun) (core : Noun) (arm : Noun), tail = (Noun.atom ax).cell c ∧ EvP subj c core ∧ Noun.slot ax core = some arm ∧ EvP core arm x

theorem Nock.Verb.EvP_op10 {subj tail x : Noun} : EvP subj ((Noun.atom 10).cell tail) x ↔ ∃ (ax : ℕ) (c : Noun) (d : Noun) (new : Noun) (old : Noun), tail = ((Noun.atom ax).cell c).cell d ∧ EvP subj c new ∧ EvP subj d old ∧ Noun.edit ax new old = some x

DenP node characterizations (paper-denotation analogues of the Den_* family)

theorem Nock.Verb.DenP_leaf {k : ℕ} {x : Noun} : (leaf k).DenP x ↔ x = Noun.atom k

theorem Nock.Verb.DenP_null {l r : Verb} {x : Noun} : (node Action.null l r).DenP x ↔ ∃ (a : Noun) (b : Noun), x = a.cell b ∧ l.DenP a ∧ r.DenP b

theorem Nock.Verb.DenP_star {l r : Verb} {x : Noun} : (node Action.star l r).DenP x ↔ ∃ (a : Noun) (b : Noun), l.DenP a ∧ r.DenP b ∧ EvP a b x

theorem Nock.Verb.DenP_slot {l r : Verb} {x : Noun} : (node Action.slot l r).DenP x ↔ ∃ (ax : ℕ) (b : Noun), l.DenP (Noun.atom ax) ∧ r.DenP b ∧ Noun.slot ax b = some x

theorem Nock.Verb.DenP_equal {l r : Verb} {x : Noun} : (node Action.equal l r).DenP x ↔ ∃ (a : Noun) (b : Noun), l.DenP a ∧ r.DenP b ∧ x = a.tis b

theorem Nock.Verb.DenP_minus {l r : Verb} {x : Noun} : (node Action.minus l r).DenP x ↔ ∃ (b : Noun), r.DenP b ∧ (l.DenP (Noun.atom 3) ∧ x = b.wut ∨ l.DenP (Noun.atom 4) ∧ b.lus = some x)

theorem Nock.Verb.DenP_edit_node {l : Verb} {b : Action} {nw od : Verb} {x : Noun} : (node Action.edit l (node b nw od)).DenP x ↔ ∃ (ax : ℕ) (n : Noun) (o : Noun), l.DenP (Noun.atom ax) ∧ nw.DenP n ∧ od.DenP o ∧ Noun.edit ax n o = some x

theorem Nock.Verb.DenP_edit_leaf {l : Verb} {k : ℕ} {x : Noun} : ¬(node Action.edit l (leaf k)).DenP x

theorem Nock.Verb.DenP_wut {l r : Verb} {x : Noun} : ¬(node Action.wut l r).DenP x

theorem Nock.Verb.DenP_terminal_iff {v : Verb} {x : Noun} (ht : v.isTerminal = true) : v.DenP x ↔ x = v.noun

The OP₁₁ hint macro (reduction-time desugaring into OP₇/OP₈)

def Nock.Verb.isHintRedex : Verb → Bool

Is v an OP₁₁ hint redex? A *-node whose formula head is the atom 11, with subject and formula-tail in terminal state, and whose tail n2 is a cell ([t d] — a hint with a body d). This is the OP₁₁ analogue of inOpcodeDomain (which rejects 11 via opHeadOk, op < 11), and is aligned exactly with hintExpand's success set: isHintRedex v = true iff hintExpand v is some.

Equations

• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 11) (Nock.Verb.node rn h b))).isHintRedex = (n1.isTerminal && ra.isNull && (Nock.Verb.node rn h b).isTerminal)
• x✝.isHintRedex = false

def Nock.Verb.hintExpand : Verb → Option Verb

Reduction-time hint expansion. Rewrite an OP₁₁ redex into its paper-opcode macro: a dynamic hint *[n1 11 [t c] d] becomes *[n1 8 c [7 [0 3] d]] (evaluate the clue c against n1, pair with n1, project n1 back out via /[3], then run the body d); a static hint *[n1 11 t d] (atom tag t) becomes *[n1 d]. Non-OP₁₁ verbs map to none.

Equations

• One or more equations did not get rendered due to their size.
• (Nock.Verb.node Nock.Action.star n1 (Nock.Verb.node ra (Nock.Verb.leaf 11) n2)).hintExpand = if (n1.isTerminal && ra.isNull && n2.isTerminal) = true then none else none
• x✝.hintExpand = none

def Nock.Verb.redexHint (v : Verb) : Option Verb

The extended local rewrite: expand an OP₁₁ hint redex (hintExpand), otherwise the standard paper local rewrite reduce (opcode redex on a *-node, or an operator-application step). Additive: redex/reduce themselves are untouched.

Equations

• v.redexHint = match v.hintExpand with | some v' => some v' | none => v.reduce

def Nock.Verb.inDomainHint (v : Verb) : Bool

The extended transition domain: inDomain plus OP₁₁ hint redexes.

Equations

• v.inDomainHint = (v.inDomain || v.isHintRedex)

def Nock.Verb.nextHint (v : Verb) : Option Verb

One step of the OP₁₁-extended Nock machine: exactly next, but with the extended domain inDomainHint and the extended local rewrite redexHint (so a selected OP₁₁ hint redex expands to its OP₇/OP₈ macro instead of crashing).

Equations

• One or more equations did not get rendered due to their size.

def Nock.Verb.runHint : ℕ → Verb → Option Noun

Fuel-indexed iteration of nextHint to a terminal/⊥ state (the OP₁₁-extended run).

Equations

• Nock.Verb.runHint 0 x✝ = none
• Nock.Verb.runHint fuel.succ x✝ = match x✝.nextHint with | some v' => Nock.Verb.runHint fuel v' | none => x✝.result

def Nock.Verb.runHintProgram (fuel : ℕ) (subject formula : Noun) : Option Noun

Run a Nock program *[subject, formula] through the OP₁₁-extended machine.

Equations

• Nock.Verb.runHintProgram fuel subject formula = Nock.Verb.runHint fuel (Nock.Verb.program subject formula)

OP₁₁ soundness

theorem Nock.Verb.reduce_none_of_isHintRedex {sub : Verb} (h : sub.isHintRedex = true) : sub.reduce = none

A hint redex is not a paper redex: reduce crashes on it. An OP₁₁ head fails opHeadOk (op < 11), so the paper local rewrite redex/reduce returns ⊥. This is what forces the extended domain to be inDomain ∨ isHintRedex, disjointly.

theorem Nock.Verb.Den_star_terminal {n1 t : Verb} {x : Noun} (h1 : n1.isTerminal = true) (ht : t.isTerminal = true) : (node Action.star n1 t).Den x ↔ Ev n1.noun t.noun x

Big-step denotation of a *-node with both children terminal is evalN of the two underlying nouns.

theorem Nock.Verb.EvN_op11_dyn {subj tb clue body x : Noun} : Ev subj ((Noun.atom 11).cell ((tb.cell clue).cell body)) x ↔ (∃ (cv : Noun), Ev subj clue cv) ∧ Ev subj body x

evalN OP₁₁ dynamic clause, as a big-step equivalence: *[a 11 [t c] d] succeeds iff the clue c converges and the body d yields the result (the clue value is discarded).

theorem Nock.Verb.EvN_op11_static {subj : Noun} {t : ℕ} {body x : Noun} : Ev subj ((Noun.atom 11).cell ((Noun.atom t).cell body)) x ↔ Ev subj body x

evalN OP₁₁ static clause, as a big-step equivalence: *[a 11 t d] = *[a d].

theorem Nock.Verb.EvN_macro_dyn {subj clue body x : Noun} : Ev subj ((Noun.atom 8).cell (clue.cell ((Noun.atom 7).cell (((Noun.atom 0).cell (Noun.atom 3)).cell body)))) x ↔ (∃ (cv : Noun), Ev subj clue cv) ∧ Ev subj body x

The dynamic-hint macro *[a 8 c [7 [0 3] d]] has the same big-step value as OP₁₁: evaluate the clue c, keep the original subject a via /[3], then run the body d.

theorem Nock.Verb.denHint_expand {sub e : Verb} {x : Noun} (he : sub.hintExpand = some e) : sub.Den x ↔ e.Den x

Hint expansion preserves den: Den sub x ↔ Den e x (OP₁₁ analogue of den_local).

theorem Nock.Verb.editOk_of_terminal {v : Verb} : v.isTerminal = true → v.editOk = true

A terminal verb (all actions ⊥) is trivially edit-well-formed.

theorem Nock.Verb.editOk_hintExpand {sub e : Verb} (he : sub.hintExpand = some e) : e.editOk = true

hintExpand produces an edit-well-formed verb (its pieces n1, clue, body are terminal).

theorem Nock.Verb.denHint_local {sub r₀ : Verb} {x : Noun} (hd : sub.inDomainHint = true) (hr : sub.redexHint = some r₀) : sub.Den x ↔ r₀.Den x

redexHint (hint expand, else reduce) preserves den.

theorem Nock.Verb.editOk_redexHint {sub r₀ : Verb} (hr : sub.redexHint = some r₀) (hok : sub.editOk = true) : r₀.editOk = true

editOk is preserved by the extended local rewrite.

theorem Nock.Verb.nextHint_eq_some_iff {a b : Verb} : a.nextHint = some b ↔ ∃ (i : ℕ) (sub : Verb) (r : Verb), IsMaxPending dfsLt a i ∧ map i a = some sub ∧ sub.inDomainHint = true ∧ sub.redexHint = some r ∧ b = replaceAt i a r

nextHint realizes the strict DFS selection step over inDomainHint/redexHint (OP₁₁ analogue of next_eq_some_iff).

theorem Nock.Verb.editOk_nextHint {v v' : Verb} (h : v.nextHint = some v') (hok : v.editOk = true) : v'.editOk = true

editOk is preserved by nextHint (the invariant discharging denHint_step).

theorem Nock.Verb.denHint_step {v v' : Verb} (hwf : v.editOk = true) (h : v.nextHint = some v') {r : Noun} : (∃ (fuel : ℕ), den fuel v = some r) ↔ ∃ (fuel : ℕ), den fuel v' = some r

One nextHint step preserves den.

theorem Nock.Verb.runHint_sound {v : Verb} {r : Noun} (fuel : ℕ) : v.editOk = true → runHint fuel v = some r → ∃ (f : ℕ), den f v = some r

Iterating nextHint to a terminal state computes den.

theorem Nock.Verb.runHintProgram_sound {s f r : Noun} {fuel : ℕ} (h : runHintProgram fuel s f = some r) : ∃ (fuel' : ℕ), evalN fuel' s f = some r

Whenever runHintProgram returns a value, evalN agrees.

Concrete OP₁₁ boundary witnesses

def Nock.Verb.hintProgStatic : Noun

Static hint *[42 11 33 0 1] = 42 (evaluate-and-discard atom tag 33, then /[1] = 42).

Equations

• Nock.Verb.hintProgStatic = (Nock.Noun.atom 11).cell ((Nock.Noun.atom 33).cell ((Nock.Noun.atom 0).cell (Nock.Noun.atom 1)))

def Nock.Verb.hintProgDyn : Noun

Dynamic hint *[42 11 [1 1 33] 0 1] = 42 (clue [1 33] computed then discarded).

Equations

• Nock.Verb.hintProgDyn = (Nock.Noun.atom 11).cell (((Nock.Noun.atom 1).cell ((Nock.Noun.atom 1).cell (Nock.Noun.atom 33))).cell ((Nock.Noun.atom 0).cell (Nock.Noun.atom 1)))

def Nock.Verb.hintProgInc : Noun

Dynamic hint over an increment: *[42 11 [1 1 33] 4 0 1] = 43.

Equations

• One or more equations did not get rendered due to their size.

theorem Nock.Verb.star_pending_is_root {L R : Verb} (hL : L.isTerminal = true) (hR : R.isTerminal = true) {i : ℕ} {sub : Verb} (hmap : map i (node Action.star L R) = some sub) (hp : sub.isPending = true) : sub = node Action.star L R

A *-node with terminal children has only its root pending. If map i retrieves a pending node from *[L, R] with L, R terminal, that node is the root itself.

theorem Nock.Verb.next_hintProg_none (subj n2 : Noun) : (program subj ((Noun.atom 11).cell n2)).next = none

The paper machine crashes at the root OP₁₁ redex of a hint program: next of the program verb is ⊥, because an OP₁₁ head is out of the paper domain (opHeadOk, op < 11) and the root *-node carries no operator.

theorem Nock.Verb.runProgram_hint_crash (subj n2 : Noun) (fuel : ℕ) : runProgram fuel subj ((Noun.atom 11).cell n2) = none

Paper machine crashes on hints (all fuel). For every fuel budget, runProgram of a hint program *[subj 11 …] is ⊥: the very first step crashes (OP₁₁ ∉ paper domain), and the crashed root *-verb is not terminal, so result is ⊥.

theorem Nock.Verb.runHint_hintStatic : runHintProgram 32 (Noun.atom 42) hintProgStatic = some (Noun.atom 42)

theorem Nock.Verb.runHint_hintDyn : runHintProgram 64 (Noun.atom 42) hintProgDyn = some (Noun.atom 42)

theorem Nock.Verb.runHint_hintInc : runHintProgram 64 (Noun.atom 42) hintProgInc = some (Noun.atom 43)

theorem Nock.Verb.paper_hint_separation : (∀ (fuel : ℕ), runProgram fuel (Noun.atom 42) hintProgStatic = none) ∧ ∃ (fuel : ℕ), runHintProgram fuel (Noun.atom 42) hintProgStatic = some (Noun.atom 42)

On *[42 11 33 0 1], runProgram crashes at every fuel while runHint yields 42.

theorem Nock.Verb.evalProgram_hint_crash (subj n2 : Noun) : evalProgram 1 subj ((Noun.atom 11).cell n2) = Outcome.crash

Positive verifiable crash. A *[subj 11 …] program — a non-opcode head atom 11 (11 ∉ [11] = {0,…,10}, main.tex:1052,1083), outside the paper's opcode domain — reports Outcome.crash under eval, not merely none under run: the first step is stuck (next_hintProg_none) and the crashed *-root is non-terminal, so haltOutcome is crash. By eval_crash_invalid the evaluated program is Invalid (the paper's ⊥, main.tex:1124), not fuel exhaustion.

theorem Nock.Verb.paper_hint_separation_crash : evalProgram 1 (Noun.atom 42) hintProgStatic = Outcome.crash ∧ ∃ (fuel : ℕ), runHintProgram fuel (Noun.atom 42) hintProgStatic = some (Noun.atom 42)

Sharpened separation: eval reports a positive crash on the non-opcode-head program while runHint yields 42 — "provably crashes", not just "produces no value".

Soundness and completeness interfaces

def Nock.Verb.HintComplete : Prop

Every successful evalN evaluation is realized by runHintProgram.

Equations

• Nock.Verb.HintComplete = ∀ (s f r : Nock.Noun), (∃ (fuel : ℕ), Nock.evalN fuel s f = some r) → ∃ (fuel : ℕ), Nock.Verb.runHintProgram fuel s f = some r

def Nock.Verb.PaperComplete : Prop

Every successful evalPaper evaluation is realized by runProgram.

Equations

• Nock.Verb.PaperComplete = ∀ (s f r : Nock.Noun), (∃ (fuel : ℕ), Nock.evalPaper fuel s f = some r) → ∃ (fuel : ℕ), Nock.Verb.runProgram fuel s f = some r

def Nock.Verb.PaperSound : Prop

Every successful runProgram evaluation is realized by evalPaper.

Equations

• Nock.Verb.PaperSound = ∀ (s f r : Nock.Noun), (∃ (fuel : ℕ), Nock.Verb.runProgram fuel s f = some r) → ∃ (fuel : ℕ), Nock.evalPaper fuel s f = some r

OP₀–OP₁₀ soundness replay

theorem Nock.Verb.DenP_ofNoun_iff {n x : Noun} : (ofNoun n).DenP x ↔ x = n

Paper-denotation analogue of Den_ofNoun_iff (helper).

theorem Nock.Verb.den_localP_opReady {sub r₀ : Verb} {x : Noun} (hor : sub.opReady = true) (hr : sub.reduce = some r₀) : sub.DenP x ↔ r₀.DenP x

theorem Nock.Verb.den_localP_opcode {sub r₀ : Verb} {x : Noun} (hd : sub.inOpcodeDomain = true) (hr : sub.reduce = some r₀) : sub.DenP x ↔ r₀.DenP x

inductive Nock.Verb.RelP : Verb → Verb → Prop

Congruence generated by equal denotations of pending subverbs in the paper fragment.

• leaf {k : ℕ} : (Verb.leaf k).RelP (Verb.leaf k)
• base {v w : Verb} : v.isPending = true → (∀ (x : Noun), v.DenP x ↔ w.DenP x) → v.RelP w
• cong {a : Action} {l l' r r' : Verb} : l.RelP l' → r.RelP r' → (node a l r).RelP (node a l' r')

theorem Nock.Verb.RelP.refl (v : Verb) : v.RelP v

theorem Nock.Verb.replaceAux_relP (i : ℕ) (r₀ v : Verb) (c : ℕ) : (∀ (sub : Verb), findAt i (v.enum c).2 = some sub → sub.isPending = true ∧ ∀ (x : Noun), sub.DenP x ↔ r₀.DenP x) → v.RelP (replaceAux i r₀ v c).2

theorem Nock.Verb.Rel_denP (n : ℕ) (v w : Verb) : v.noun.size ≤ n → v.RelP w → v.editOk = true → ∀ (x : Noun), v.DenP x ↔ w.DenP x

theorem Nock.Verb.den_localP {sub r₀ : Verb} {x : Noun} (hd : sub.inDomain = true) (hr : sub.reduce = some r₀) : sub.DenP x ↔ r₀.DenP x

theorem Nock.Verb.den_stepP {v v' : Verb} (hwf : v.editOk = true) (h : v.next = some v') {r : Noun} : (∃ (fuel : ℕ), denP fuel v = some r) ↔ ∃ (fuel : ℕ), denP fuel v' = some r

theorem Nock.Verb.run_soundP {v : Verb} {r : Noun} (fuel : ℕ) : v.editOk = true → run fuel v = some r → ∃ (f : ℕ), denP f v = some r

theorem Nock.Verb.paperSound_holds : PaperSound

runProgram soundness against the derived OP₀–OP₁₀ oracle.

theorem Nock.Verb.runHint_adequate (hc : HintComplete) (s f r : Noun) : (∃ (fuel : ℕ), runHintProgram fuel s f = some r) ↔ ∃ (fuel : ℕ), evalN fuel s f = some r

Conditional wrapper for OP₁₁ adequacy (see runHint_adequate_complete).

Progress (denP-defined + non-terminal ⇒ next fires)

theorem Nock.Verb.denP_left_defined {a : Action} {l r : Verb} {f : ℕ} {x : Noun} (h : denP (f + 1) (node a l r) = some x) : ∃ (y : Noun), denP f l = some y

denP of a */operator node forces the LEFT child to be denP-defined.

theorem Nock.Verb.denP_right_defined_of_editOk {a : Action} {l r : Verb} {f : ℕ} {x : Noun} (hok : (node a l r).editOk = true) (h : denP (f + 1) (node a l r) = some x) : ∃ (g : ℕ) (y : Noun), denP g r = some y

denP of an editOk node forces the RIGHT child to be denP-defined (the edit case uses editOk: its right child is non-pending, hence a ⊥-cons of its two denP-defined args).

theorem Nock.Verb.enum_denP_defined (v : Verb) : v.editOk = true → ∀ (c f : ℕ) (x : Noun), denP f v = some x → ∀ p ∈ (v.enum c).2, ∃ (g : ℕ) (y : Noun), denP g p.2 = some y

denP-definedness descends to every enumerated subnode (given editOk).

theorem Nock.Verb.DenP_subnode {v : Verb} {x : Noun} (hok : v.editOk = true) (hv : v.DenP x) {i : ℕ} {sub : Verb} (hmap : map i v = some sub) : ∃ (y : Noun), sub.DenP y

The subnode map i v = some sub of a denP-defined editOk verb is itself denP-defined.

theorem Nock.Verb.evalPaper_atom_none (f : ℕ) (s : Noun) (k : ℕ) : evalPaper f s (Noun.atom k) = none

evalPaper crashes when the formula is an atom (bare noun, no opcode).

theorem Nock.Verb.evalPaper_op_ge11 (f : ℕ) (s tail : Noun) (op : ℕ) (h : 11 ≤ op) : evalPaper f s ((Noun.atom op).cell tail) = none

evalPaper crashes on an out-of-fragment opcode head (op ≥ 11).

theorem Nock.Verb.inDomain_star_of {L I n2 : Verb} {rb : Action} (hL : L.isTerminal = true) (hrb : rb.isNull = true) (hI : I.isTerminal = true) (hn2 : n2.isTerminal = true) (hhead : I.opHeadOk = true) : (node Action.star L (node rb I n2)).inDomain = true

A *-redex with terminal children and a valid opcode head is in the transition domain.

theorem Nock.Verb.progressP {v : Verb} {x : Noun} (hwf : v.editOk = true) (hd : v.DenP x) (hnt : v.isTerminal = false) : ∃ (v' : Verb), v.next = some v'

A denP-defined, editOk, non-terminal verb has a next successor.

Denotation-keyed cost measure

def Nock.Verb.pcost : ℕ → Noun → Noun → ℕ

Weighted evalPaper-derivation cost: mirrors evalPaper clause-for-clause (same recursive calls), each opcode contributing a positive weight. Returns 0 where evalPaper crashes.

Equations

• One or more equations did not get rendered due to their size.
• Nock.Verb.pcost 0 x✝¹ x✝ = 0
• Nock.Verb.pcost n.succ x✝ (Nock.Noun.atom a) = 0
• Nock.Verb.pcost f.succ x✝ ((b.cell c).cell d) = 1 + Nock.Verb.pcost f x✝ (b.cell c) + Nock.Verb.pcost f x✝ d
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 0).cell tail) = 2
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 1).cell tail) = 1
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 2).cell tail) = 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 3).cell tail) = 2 + Nock.Verb.pcost f x✝ tail
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 4).cell tail) = 2 + Nock.Verb.pcost f x✝ tail
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 5).cell (b.cell c)) = 2 + Nock.Verb.pcost f x✝ b + Nock.Verb.pcost f x✝ c
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 5).cell tail) = 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 6).cell tail) = 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 7).cell (b.cell c)) = 1 + Nock.Verb.pcost f x✝ b + match Nock.evalPaper f x✝ b with | some sb => Nock.Verb.pcost f sb c | x => 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 7).cell tail) = 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 8).cell (b.cell c)) = 1 + Nock.Verb.pcost f x✝ b + match Nock.evalPaper f x✝ b with | some sb => Nock.Verb.pcost f (sb.cell x✝) c | x => 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 8).cell tail) = 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 9).cell tail) = 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 10).cell (((Nock.Noun.atom a).cell c).cell d)) = 2 + Nock.Verb.pcost f x✝ c + Nock.Verb.pcost f x✝ d
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom 10).cell tail) = 0
• Nock.Verb.pcost f.succ x✝ ((Nock.Noun.atom op).cell tail) = 0

def Nock.Verb.vcost (F : ℕ) : Verb → ℕ

Verb cost (structural in the verb; F is a fixed lookup-fuel for denotations). A *-node charges pcost of its two denotations (the firing cost); an operator node charges 1; ⊥/leaf charge only their children. Being structural (not fuel-recursive), replaceAt swaps exactly one subtree's cost, so the step-congruence is immediate.

Equations

• One or more equations did not get rendered due to their size.
• Nock.Verb.vcost F (Nock.Verb.leaf a) = 0
• Nock.Verb.vcost F (Nock.Verb.node Nock.Action.slot l r) = 1 + Nock.Verb.vcost F l + Nock.Verb.vcost F r
• Nock.Verb.vcost F (Nock.Verb.node Nock.Action.equal l r) = 1 + Nock.Verb.vcost F l + Nock.Verb.vcost F r
• Nock.Verb.vcost F (Nock.Verb.node Nock.Action.minus l r) = 1 + Nock.Verb.vcost F l + Nock.Verb.vcost F r
• Nock.Verb.vcost F (Nock.Verb.node Nock.Action.edit l r) = 1 + Nock.Verb.vcost F l + Nock.Verb.vcost F r
• Nock.Verb.vcost F (Nock.Verb.node Nock.Action.null l r) = 0 + Nock.Verb.vcost F l + Nock.Verb.vcost F r
• Nock.Verb.vcost F (Nock.Verb.node Nock.Action.wut l r) = 0 + Nock.Verb.vcost F l + Nock.Verb.vcost F r

theorem Nock.Verb.pcost_succ {n : ℕ} {a b r : Noun} (hb : evalPaper n a b = some r) : pcost (n + 1) a b = pcost n a b

pcost is unchanged by extra fuel once evalPaper succeeds (mirrors evalPaper_succ).

theorem Nock.Verb.pcost_mono {n m : ℕ} {a b r : Noun} (hle : n ≤ m) (hb : evalPaper n a b = some r) : pcost m a b = pcost n a b

pcost stabilizes for any fuel ≥ n once evalPaper n succeeds.

theorem Nock.Verb.vcost_terminal (v : Verb) : v.isTerminal = true → ∀ (F : ℕ), vcost F v = 0

vcost of a terminal verb is 0.

theorem Nock.Verb.runProgram_adequate (hc : PaperComplete) (s f r : Noun) : (∃ (fuel : ℕ), runProgram fuel s f = some r) ↔ ∃ (fuel : ℕ), evalPaper fuel s f = some r

Conditional wrapper for OP₀–OP₁₀ consistency (see runProgram_adequate_complete).