nx_autoformalize_lib.nx source
↩ module page · 408 lines · 19392 B
1// nx_autoformalize_lib.nx -- the CANONICAL autoformalization library (pure funcs, no main), extracted
2// 2026-07-15 from nx_autoformalize.nx so other organs can compose the verifier (the propose->verify loop:
3// an LLM PROPOSES, this kernel-backed checker DISPOSES). Same code, zero behavior change; the organ's own
4// gate battery re-proves it after the split.
5// af_decide(claim, vb) -> 1 PROVED · 2 REFUTED · 3 UNSUPPORTED · 5 NO-SOLUTION · -1 kernel failure
6// Grammar: "<n|what> [plus|times <n|what>] =|equals|is|<|under|<= <n>", digits or words zero..twelve;
7// plus operands <= 12, times operands <= 6, rhs <= 144. Everything derives through the LCF v2 kernel
8// (nx_k2_verify checks the whole chain; a wrong claim CANNOT certify -- soundness by construction).
9// license_tier: ORIGINAL (lib: no main -- build standalone gives rc=102 by design)
10import "nx_arith.nx"
11
12func af_w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
13func af_n(v: i64) -> i64 {
14 var m: i64 = v
15 if m < 0 { af_w("-" as *u8); m = 0 - m }
16 let t: *u8 = sys_mmap(24)
17 var k: i64 = 0
18 if m == 0 { t[0] = 48 as u8; k = 1 }
19 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
20 let o: *u8 = sys_mmap(24)
21 var i: i64 = 0
22 while i < k { o[i] = t[k - 1 - i]; i = i + 1 }
23 sys_write(1, o, k)
24 return 0
25}
26func af_streq(a: *u8, b: *u8) -> i64 { var i: i64 = 0; while a[i] != (0 as u8) { if a[i] != b[i] { return 0 } i = i + 1 } if b[i] != (0 as u8) { return 0 } return 1 }
27
28// number-word lexicon zero..twelve -> value, else -1; pure digits -> value; else -1.
29func af_tok_num(t: *u8) -> i64 {
30 var alldig: i64 = 1
31 var i: i64 = 0
32 var v: i64 = 0
33 while t[i] != (0 as u8) {
34 let c: i64 = t[i] as i64
35 if c >= 48 { if c <= 57 { v = v * 10 + (c - 48); i = i + 1 } else { alldig = 0; i = i + 1 } } else { alldig = 0; i = i + 1 }
36 }
37 if i > 0 { if alldig == 1 { return v } }
38 if af_streq(t, "zero" as *u8) == 1 { return 0 }
39 if af_streq(t, "one" as *u8) == 1 { return 1 }
40 if af_streq(t, "two" as *u8) == 1 { return 2 }
41 if af_streq(t, "three" as *u8) == 1 { return 3 }
42 if af_streq(t, "four" as *u8) == 1 { return 4 }
43 if af_streq(t, "five" as *u8) == 1 { return 5 }
44 if af_streq(t, "six" as *u8) == 1 { return 6 }
45 if af_streq(t, "seven" as *u8) == 1 { return 7 }
46 if af_streq(t, "eight" as *u8) == 1 { return 8 }
47 if af_streq(t, "nine" as *u8) == 1 { return 9 }
48 if af_streq(t, "ten" as *u8) == 1 { return 10 }
49 if af_streq(t, "eleven" as *u8) == 1 { return 11 }
50 if af_streq(t, "twelve" as *u8) == 1 { return 12 }
51 return 0 - 1
52}
53func af_tok_plus(t: *u8) -> i64 { if af_streq(t, "+" as *u8) == 1 { return 1 } if af_streq(t, "plus" as *u8) == 1 { return 1 } return 0 }
54func af_tok_times(t: *u8) -> i64 { if af_streq(t, "*" as *u8) == 1 { return 1 } if af_streq(t, "times" as *u8) == 1 { return 1 } return 0 }
55func af_tok_eqw(t: *u8) -> i64 { if af_streq(t, "=" as *u8) == 1 { return 1 } if af_streq(t, "equals" as *u8) == 1 { return 1 } if af_streq(t, "is" as *u8) == 1 { return 1 } return 0 }
56func af_tok_lt(t: *u8) -> i64 { if af_streq(t, "<" as *u8) == 1 { return 1 } if af_streq(t, "under" as *u8) == 1 { return 1 } return 0 }
57func af_tok_unknown(t: *u8) -> i64 { if af_streq(t, "what" as *u8) == 1 { return 1 } if af_streq(t, "x" as *u8) == 1 { return 1 } return 0 }
58func af_tok_le(t: *u8) -> i64 { if af_streq(t, "<=" as *u8) == 1 { return 1 } return 0 }
59
60// parse a claim (space-tokenized) into res[0..5]: res[0]=a res[1]=op(0 none|1 plus|2 times) res[2]=b
61// res[3]=rel(1 eq|2 lt|3 le) res[4]=c res[5]=unknown-slot(0 none|1 a|2 b).
62// forms: "<n> <rel> <n>" (op 0)
63// "<n|what> <plus|times> <n|what> <rel> <n>" (ONE unknown allowed, eq only -- rung 4 solve-forms)
64// rel: = / equals / is (1) · < / under (2) · <= (3). ("is under" works: eq collapses before a rel token;
65// unknown words are skipped.) 1 ok, 0 unsupported.
66func af_parse(s: *u8, res: *i64) -> i64 {
67 // named views into the result array (avoids a 7-arg signature -- the >6-arg clobber trap)
68 let abox: *i64 = ((res as i64) + 0) as *i64
69 let opbox: *i64 = ((res as i64) + 8) as *i64
70 let bbox: *i64 = ((res as i64) + 16) as *i64
71 let relbox: *i64 = ((res as i64) + 24) as *i64
72 let cbox: *i64 = ((res as i64) + 32) as *i64
73 let ubox: *i64 = ((res as i64) + 40) as *i64
74 ubox[0] = 0
75 let tok: *u8 = sys_mmap(64)
76 let vals: *i64 = sys_mmap(64) as *i64
77 let kinds: *i64 = sys_mmap(64) as *i64 // 1=num 2=plus 3=eq 4=times 5=lt 6=le
78 var nt: i64 = 0
79 var i: i64 = 0
80 var run: i64 = 1
81 while run == 1 {
82 while s[i] == (32 as u8) { i = i + 1 }
83 if s[i] == (0 as u8) { run = 0 } else {
84 var p: i64 = 0
85 while s[i] != (0 as u8) { if s[i] == (32 as u8) { break } if p < 62 { tok[p] = s[i]; p = p + 1 } i = i + 1 }
86 tok[p] = 0 as u8
87 let nv: i64 = af_tok_num(tok)
88 var kind: i64 = 0
89 var val: i64 = 0
90 if nv >= 0 { kind = 1; val = nv } else {
91 if af_tok_plus(tok) == 1 { kind = 2 } else {
92 if af_tok_times(tok) == 1 { kind = 4 } else {
93 if af_tok_le(tok) == 1 { kind = 6 } else {
94 if af_tok_lt(tok) == 1 { kind = 5 } else {
95 if af_tok_unknown(tok) == 1 { kind = 7 } else { if af_tok_eqw(tok) == 1 { kind = 3 } }
96 }
97 }
98 }
99 }
100 }
101 if kind != 0 { if nt < 8 { kinds[nt] = kind; vals[nt] = val; nt = nt + 1 } }
102 }
103 }
104 // collapse "is <" / "is <=" (eq token immediately followed by a rel token)
105 var w2: i64 = 0
106 var r2: i64 = 0
107 while r2 < nt {
108 var drop: i64 = 0
109 if kinds[r2] == 3 { if r2 + 1 < nt { if kinds[r2 + 1] == 5 { drop = 1 } if kinds[r2 + 1] == 6 { drop = 1 } } }
110 if drop == 0 { kinds[w2] = kinds[r2]; vals[w2] = vals[r2]; w2 = w2 + 1 }
111 r2 = r2 + 1
112 }
113 nt = w2
114 var rel: i64 = 0
115 if nt == 3 {
116 if kinds[0] != 1 { return 0 }
117 if kinds[1] == 3 { rel = 1 }
118 if kinds[1] == 5 { rel = 2 }
119 if kinds[1] == 6 { rel = 3 }
120 if rel == 0 { return 0 }
121 if kinds[2] != 1 { return 0 }
122 if vals[0] > 144 { return 0 }
123 if vals[2] > 144 { return 0 }
124 abox[0] = vals[0]
125 opbox[0] = 0
126 bbox[0] = 0
127 relbox[0] = rel
128 cbox[0] = vals[2]
129 return 1
130 }
131 if nt != 5 { return 0 }
132 var unk: i64 = 0
133 if kinds[0] == 7 { unk = 1 } else { if kinds[0] != 1 { return 0 } }
134 var op: i64 = 0
135 if kinds[1] == 2 { op = 1 }
136 if kinds[1] == 4 { op = 2 }
137 if op == 0 { return 0 }
138 if kinds[2] == 7 { if unk != 0 { return 0 } unk = 2 } else { if kinds[2] != 1 { return 0 } }
139 if kinds[3] == 3 { rel = 1 }
140 if kinds[3] == 5 { rel = 2 }
141 if kinds[3] == 6 { rel = 3 }
142 if rel == 0 { return 0 }
143 if unk != 0 { if rel != 1 { return 0 } } // solve-forms are eq-only (rung 4)
144 if kinds[4] != 1 { return 0 }
145 if unk != 1 { if vals[0] > 12 { return 0 } }
146 if unk != 2 { if vals[2] > 12 { return 0 } }
147 if op == 2 { if unk != 1 { if vals[0] > 6 { return 0 } } }
148 if op == 2 { if unk != 2 { if vals[2] > 6 { return 0 } } }
149 if vals[4] > 144 { return 0 }
150 abox[0] = vals[0]
151 opbox[0] = op
152 bbox[0] = vals[2]
153 relbox[0] = rel
154 cbox[0] = vals[4]
155 ubox[0] = unk
156 return 1
157}
158
159// build the relation Term App(sym, [x, y]) (the nx_arith_plus copy-args pattern; nx_arith reserves LT/LE syms).
160func af_rel_term(sym: i64, x: *Term, y: *Term) -> *Term {
161 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
162 let a0: *Term = args
163 a0.kind = x.kind; a0.sym = x.sym; a0.n_args = x.n_args; a0.args = x.args
164 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
165 a1.kind = y.kind; a1.sym = y.sym; a1.n_args = y.n_args; a1.args = y.args
166 return nx_term_app(sym, 2, args)
167}
168
169// DERIVE lt(nat u, nat v) for concrete u < v: the exists-witness DEFINITIONAL instance. First derive the
170// witness sum plus(u, v-u) = v through the kernel (v-u >= 1, so the addend is a genuine succ-numeral), then
171// MP the instance axiom eq(plus(u, v-u), v) => lt(u, v).
172func af_derive_lt(ch: *K2Chain, u: i64, v: i64, stepsbox: *i64) -> i64 {
173 if u >= v { return 0 - 1 }
174 let sb: *i64 = sys_mmap(8) as *i64
175 sb[0] = 0
176 let sum: i64 = af_derive_sum(ch, u, v - u, sb)
177 if sum < 0 { return 0 - 1 }
178 let def: i64 = nx_k2_axiom(ch, nx_k2_imp(
179 nx_k2_eq(nx_arith_plus(nx_arith_nat(u), nx_arith_nat(v - u)), nx_arith_nat(v)),
180 af_rel_term(NX_ARITH_SYM_LT, nx_arith_nat(u), nx_arith_nat(v))))
181 if def < 0 { return 0 - 1 }
182 let r: i64 = nx_k2_modus_ponens(ch, def, sum)
183 if r < 0 { return 0 - 1 }
184 stepsbox[0] = sb[0] + 2
185 return r
186}
187
188// DERIVE le(nat u, nat v) for concrete u <= v: u==v goes via kernel REFL + the eq=>le instance; u<v goes via
189// the lt derivation + the lt=>le instance.
190func af_derive_le(ch: *K2Chain, u: i64, v: i64, stepsbox: *i64) -> i64 {
191 if u > v { return 0 - 1 }
192 let sb: *i64 = sys_mmap(8) as *i64
193 sb[0] = 0
194 var base: i64 = 0 - 1
195 var ante: *Term = 0 as *Term
196 if u == v {
197 base = nx_k2_refl(ch, nx_arith_nat(u))
198 ante = nx_k2_eq(nx_arith_nat(u), nx_arith_nat(v))
199 sb[0] = 1
200 } else {
201 base = af_derive_lt(ch, u, v, sb)
202 ante = af_rel_term(NX_ARITH_SYM_LT, nx_arith_nat(u), nx_arith_nat(v))
203 }
204 if base < 0 { return 0 - 1 }
205 let def: i64 = nx_k2_axiom(ch, nx_k2_imp(ante, af_rel_term(NX_ARITH_SYM_LE, nx_arith_nat(u), nx_arith_nat(v))))
206 if def < 0 { return 0 - 1 }
207 let r: i64 = nx_k2_modus_ponens(ch, def, base)
208 if r < 0 { return 0 - 1 }
209 stepsbox[0] = sb[0] + 2
210 return r
211}
212
213// DERIVE eq(plus(a,b), nat(a+b)) through the kernel. Returns the theorem chain index (>=0) and fills
214// stepsbox with the number of inference steps; -1 on kernel failure. Axioms used: PA3 instance, PA4
215// instances, succ-cong instances (explicit implication axioms, MP'd -- the bootstrap-instance style).
216func af_derive_sum(ch: *K2Chain, a: i64, b: i64, stepsbox: *i64) -> i64 {
217 let na: *Term = nx_arith_nat(a)
218 var steps: i64 = 0
219 // base: PA3 instance plus(a, 0) = a
220 var cur: i64 = nx_arith_axiom_plus_zero(ch, na)
221 if cur < 0 { return 0 - 1 }
222 steps = steps + 1
223 var k: i64 = 1
224 while k <= b {
225 // PA4 instance: plus(a, k) = succ(plus(a, k-1))
226 let pa4: i64 = nx_arith_axiom_plus_succ(ch, na, nx_arith_nat(k - 1))
227 if pa4 < 0 { return 0 - 1 }
228 // succ-cong instance axiom: eq(plus(a,k-1), a+k-1) => eq(succ(plus(a,k-1)), succ(a+k-1))
229 let lhs_in: *Term = nx_k2_eq(nx_arith_plus(na, nx_arith_nat(k - 1)), nx_arith_nat(a + k - 1))
230 let lhs_out: *Term = nx_k2_eq(nx_arith_succ(nx_arith_plus(na, nx_arith_nat(k - 1))), nx_arith_nat(a + k))
231 let cong: i64 = nx_k2_axiom(ch, nx_k2_imp(lhs_in, lhs_out))
232 if cong < 0 { return 0 - 1 }
233 // MP: from cur (plus(a,k-1) = a+k-1) get succ(plus(a,k-1)) = a+k
234 let lifted: i64 = nx_k2_modus_ponens(ch, cong, cur)
235 if lifted < 0 { return 0 - 1 }
236 // trans: plus(a,k) = succ(plus(a,k-1)) = a+k
237 let nxt: i64 = nx_k2_eq_trans(ch, pa4, lifted)
238 if nxt < 0 { return 0 - 1 }
239 cur = nxt
240 steps = steps + 4
241 k = k + 1
242 }
243 stepsbox[0] = steps
244 return cur
245}
246
247// DERIVE eq(mult(a,b), nat(a*b)) through the kernel (rung 2). Peano multiplication instances:
248// M0: mult(a, 0) = 0 (mult-zero instance)
249// Mk: mult(a, k) = plus(mult(a, k-1), a) (mult-succ instance)
250// plus a plus-LEFT-congruence instance per step; every mult step then REUSES af_derive_sum for the
251// concrete addition, so a mult proof literally composes the rung-1 plus proofs. Two eq_trans stitch each step.
252func af_derive_mult(ch: *K2Chain, a: i64, b: i64, stepsbox: *i64) -> i64 {
253 let na: *Term = nx_arith_nat(a)
254 var steps: i64 = 0
255 var cur: i64 = nx_k2_axiom(ch, nx_k2_eq(nx_arith_mult(na, nx_arith_zero()), nx_arith_zero()))
256 if cur < 0 { return 0 - 1 }
257 steps = steps + 1
258 let sb: *i64 = sys_mmap(8) as *i64
259 var k: i64 = 1
260 while k <= b {
261 let ms: i64 = nx_k2_axiom(ch, nx_k2_eq(nx_arith_mult(na, nx_arith_nat(k)), nx_arith_plus(nx_arith_mult(na, nx_arith_nat(k - 1)), na)))
262 if ms < 0 { return 0 - 1 }
263 let ci: i64 = nx_k2_axiom(ch, nx_k2_imp(
264 nx_k2_eq(nx_arith_mult(na, nx_arith_nat(k - 1)), nx_arith_nat(a * (k - 1))),
265 nx_k2_eq(nx_arith_plus(nx_arith_mult(na, nx_arith_nat(k - 1)), na), nx_arith_plus(nx_arith_nat(a * (k - 1)), na))))
266 if ci < 0 { return 0 - 1 }
267 let lifted: i64 = nx_k2_modus_ponens(ch, ci, cur)
268 if lifted < 0 { return 0 - 1 }
269 let t1: i64 = nx_k2_eq_trans(ch, ms, lifted)
270 if t1 < 0 { return 0 - 1 }
271 sb[0] = 0
272 let psum: i64 = af_derive_sum(ch, a * (k - 1), a, sb)
273 if psum < 0 { return 0 - 1 }
274 let nxt: i64 = nx_k2_eq_trans(ch, t1, psum)
275 if nxt < 0 { return 0 - 1 }
276 cur = nxt
277 steps = steps + 5 + sb[0]
278 k = k + 1
279 }
280 stepsbox[0] = steps
281 return cur
282}
283
284// formalize + decide ONE claim. Returns 1 PROVED, 2 REFUTED, 3 UNSUPPORTED, -1 kernel failure.
285// When vb=1, prints the human trace.
286func af_decide(claim: *u8, vb: i64) -> i64 {
287 let res: *i64 = sys_mmap(48) as *i64
288 if af_parse(claim, res) != 1 {
289 if vb == 1 { af_w(" [UNSUPPORTED] " as *u8); af_w(claim); af_w(" (outside the grammar: <n|what> [plus|times <n|what>] =|<|<= <n>)\n" as *u8) }
290 return 3
291 }
292 var a: i64 = res[0]
293 let op: i64 = res[1]
294 var b: i64 = res[2]
295 let rel: i64 = res[3]
296 let c: i64 = res[4]
297 let unk: i64 = res[5]
298 var solved: i64 = 0 - 1
299 if unk != 0 {
300 // rung 4 SOLVE-FORM: solve the single unknown over the naturals; the derivation below is the certificate.
301 var known: i64 = b
302 if unk == 2 { known = a }
303 var sol: i64 = 0 - 1
304 if op == 1 { if c >= known { sol = c - known } }
305 if op == 2 {
306 if known == 0 { if c == 0 { sol = 0 } } else { if (c % known) == 0 { sol = c / known } }
307 }
308 if sol < 0 {
309 if vb == 1 { af_w(" [NO-SOLUTION] " as *u8); af_w(claim); af_w(" (no natural number satisfies it)\n" as *u8) }
310 return 5
311 }
312 var solcap: i64 = 12
313 if op == 2 { solcap = 6 }
314 if sol > solcap {
315 if vb == 1 { af_w(" [UNSUPPORTED] " as *u8); af_w(claim); af_w(" (solution exceeds the rung budget)\n" as *u8) }
316 return 3
317 }
318 solved = sol
319 if unk == 1 { a = sol } else { b = sol }
320 }
321 var v: i64 = a
322 if op == 1 { v = a + b }
323 if op == 2 { v = a * b }
324 var truth: i64 = 0
325 if rel == 1 { if v == c { truth = 1 } }
326 if rel == 2 { if v < c { truth = 1 } }
327 if rel == 3 { if v <= c { truth = 1 } }
328 // rung-3 chain budget: a TRUE ordering claim needs a witness sum of length (c - v); keep it derivable.
329 if rel >= 2 { if truth == 1 { if (c - v) > 12 {
330 if vb == 1 { af_w(" [UNSUPPORTED] " as *u8); af_w(claim); af_w(" (witness distance beyond the rung-3 chain budget of 12)\n" as *u8) }
331 return 3
332 } } }
333 let ch: *K2Chain = nx_k2_chain_new(256)
334 let stepsbox: *i64 = sys_mmap(8) as *i64
335 stepsbox[0] = 1
336 // expression term E + its kernel-derived value theorem eq(E, nat v)
337 var eterm: *Term = nx_arith_nat(a)
338 if op == 1 { eterm = nx_arith_plus(nx_arith_nat(a), nx_arith_nat(b)) }
339 if op == 2 { eterm = nx_arith_mult(nx_arith_nat(a), nx_arith_nat(b)) }
340 var eqthm: i64 = 0 - 1
341 if op == 0 { eqthm = nx_k2_refl(ch, nx_arith_nat(a)) } else {
342 if op == 1 { eqthm = af_derive_sum(ch, a, b, stepsbox) } else { eqthm = af_derive_mult(ch, a, b, stepsbox) }
343 }
344 if eqthm < 0 { return 0 - 1 }
345 var thm: i64 = eqthm
346 var expected: *Term = nx_k2_eq(eterm, nx_arith_nat(v))
347 // TRUE ordering claims: derive rel(nat v, nat c) then lift to rel(E, nat c) through an instance + 2 MPs.
348 if rel >= 2 { if truth == 1 {
349 var relsym: i64 = NX_ARITH_SYM_LT
350 if rel == 3 { relsym = NX_ARITH_SYM_LE }
351 let rb: *i64 = sys_mmap(8) as *i64
352 rb[0] = 0
353 var relthm: i64 = 0 - 1
354 if rel == 2 { relthm = af_derive_lt(ch, v, c, rb) } else { relthm = af_derive_le(ch, v, c, rb) }
355 if relthm < 0 { return 0 - 1 }
356 stepsbox[0] = stepsbox[0] + rb[0]
357 if op == 0 {
358 thm = relthm
359 } else {
360 let lift: i64 = nx_k2_axiom(ch, nx_k2_imp(
361 nx_k2_eq(eterm, nx_arith_nat(v)),
362 nx_k2_imp(af_rel_term(relsym, nx_arith_nat(v), nx_arith_nat(c)), af_rel_term(relsym, eterm, nx_arith_nat(c)))))
363 if lift < 0 { return 0 - 1 }
364 let m1: i64 = nx_k2_modus_ponens(ch, lift, eqthm)
365 if m1 < 0 { return 0 - 1 }
366 let m2: i64 = nx_k2_modus_ponens(ch, m1, relthm)
367 if m2 < 0 { return 0 - 1 }
368 thm = m2
369 stepsbox[0] = stepsbox[0] + 3
370 }
371 expected = af_rel_term(relsym, eterm, nx_arith_nat(c))
372 if op == 0 { expected = af_rel_term(relsym, nx_arith_nat(v), nx_arith_nat(c)) }
373 } }
374 // the kernel must accept the whole chain (mark the final node as THE theorem, then verify integrity)
375 if nx_k2_mark_theorem(ch) < 0 { return 0 - 1 }
376 if nx_k2_verify(ch) != 0 { return 0 - 1 }
377 // shape-check the derived theorem against the INDEPENDENTLY built expectation...
378 let t: *K2Thm = nx_k2_at(ch, thm)
379 if nx_term_eq(t.stmt, expected) != 1 { return 0 - 1 }
380 if t.n_hyps != 0 { return 0 - 1 }
381 // ...then compare the CLAIMED statement to the derived one
382 var relsym2: i64 = 0
383 if rel == 2 { relsym2 = NX_ARITH_SYM_LT }
384 if rel == 3 { relsym2 = NX_ARITH_SYM_LE }
385 var claimterm: *Term = nx_k2_eq(eterm, nx_arith_nat(c))
386 if rel >= 2 { claimterm = af_rel_term(relsym2, eterm, nx_arith_nat(c)) }
387 let claimed_ok: i64 = nx_term_eq(t.stmt, claimterm)
388 if vb == 1 {
389 if claimed_ok == 1 { if solved >= 0 { af_w(" [SOLVED ] " as *u8) } else { af_w(" [PROVED ] " as *u8) } } else { af_w(" [REFUTED ] " as *u8) }
390 af_w(claim)
391 if solved >= 0 { af_w(" -> x = " as *u8); af_n(solved); af_w(";" as *u8) }
392 if op == 2 { af_w(" -> mult(" as *u8); af_n(a); af_w("," as *u8); af_n(b); af_w(")" as *u8) } else {
393 if op == 1 { af_w(" -> plus(" as *u8); af_n(a); af_w("," as *u8); af_n(b); af_w(")" as *u8) } else { af_w(" -> " as *u8); af_n(a) }
394 }
395 af_w(" = " as *u8); af_n(v)
396 if claimed_ok == 1 { if rel == 2 { af_w(" < " as *u8); af_n(c) } }
397 if claimed_ok == 1 { if rel == 3 { af_w(" <= " as *u8); af_n(c) } }
398 af_w(" (kernel-checked, " as *u8); af_n(stepsbox[0]); af_w(" inference steps" as *u8)
399 if claimed_ok == 1 { af_w(")\n" as *u8) } else {
400 af_w("; the claim said " as *u8)
401 if rel == 2 { af_w("< " as *u8) }
402 if rel == 3 { af_w("<= " as *u8) }
403 af_n(c); af_w(")\n" as *u8)
404 }
405 }
406 if claimed_ok == 1 { return 1 }
407 return 2
408}