completed proof

1 files changed, 467 insertions, 447 deletions

diff --git a/proof.norg b/proof.norg
index 8ae8490..21f1fcd 100644
--- a/proof.norg
+++ b/proof.norg
@@ -4,63 +4,64 @@ description:
 authors: ericmarin
 categories: research
 created: 2026-03-16T11:34:52
-updated: 2026-03-25T08:18:04
+updated: 2026-03-28T17:37:48
 version: 1.1.1
 @end
 
-* Mathematical Definitions
-	- Linear(x, q, r) ~ out => out = q*x + r
-	- Concrete(k) ~ out => out = k
-	- Add(out, b) ~ a => out = a + b
-	- AddCheckLinear(out, x, q, r) ~ b => out = q*x + (r + b)
-	- AddCheckConcrete(out, k) ~ b => out = k + b
-	- Mul(out, b) ~ a => out = a * b
-	- MulCheckLinear(out, x, q, r) ~ b => out = q*b*x + r*b
-	- MulCheckConcrete(out, k) ~ b => out = k*b
-	- ReLU(out) ~ x => out = IF (x > 0) THEN x ELSE 0
-	- Materialize(out) ~ x => out = x
-
-* Proof for translation from Pytorch representation to Interaction Net graph
-** ReLU
-	 ONNX ReLU node is defined as:
-	 /Y = X if X > 0 else 0/
-
-	 The translation defines the interactions:
-	 /x_i ~ ReLU(y_i)/
-
-	 By definition this interaction is equal to:
-	 /y_i = IF (x_i >0) THEN x_i ELSE 0/
-
-** Gemm
-	 ONNX Gemm node is defined as:
-	 Y = alpha * A * B + beta * C
-
-	 The translation defines the interactions:
-	 /a_i ~ Mul(v_i, Concrete(alpha * b_i))/
-	 /Add(...(Add(y_i, v_1), ...), v_n) ~ Concrete(beta * c_i)/
-
-	 By definition this interaction is equal to:
-	 /v_i = alpha * a_i * b_i/
-	 /y_i = v_1 + v_2 + ... + v_n + beta * c_i/
-
-	 By grouping the operations we get:
-	 /Y = alpha * A * B + beta * C/
-
-** Flatten
-	 Just identity mapping.
-
-** MatMul
-	 Equal to Gemm with alpha=1 and beta=0.
-
-** Reshape
-	 Just identity mapping.
-
-* Proof for the Interaction Rules
-** Materialize
-	 The Materialize agent transforms a Linear agent into a tree of explicit mathematical operations
-	 that are used as final representation for the solver.
-	 In the Python module the terms are defined as:
-	 @code python
+* Soundness Proof
+** Mathematical Definitions
+	 - $Linear(x, q, r) ~ out => out = q*x + r$
+	 - $Concrete(k) ~ out => out = k$
+	 - $Add(out, b) ~ a => out = a + b$
+	 - $AddCheckLinear(out, x, q, r) ~ b => out = q*x + (r + b)$
+	 - $AddCheckConcrete(out, k) ~ b => out = k + b$
+	 - $Mul(out, b) ~ a => out = a * b$
+	 - $MulCheckLinear(out, x, q, r) ~ b => out = q*b*x + r*b$
+	 - $MulCheckConcrete(out, k) ~ b => out = k*b$
+	 - $ReLU(out) ~ x => out = IF (x > 0) THEN x ELSE 0$
+	 - $Materialize(out) ~ x => out = x$
+
+** Soundness of Translation
+*** ReLU
+		ONNX ReLU node is defined as:
+		$Y = X if X > 0 else 0$
+
+		The translation defines the interactions:
+		$x_i ~ ReLU(y_i)$
+
+		By definition this interaction is equal to:
+		$y_i = IF (x_i > 0) THEN x_i ELSE 0$
+
+*** Gemm
+		ONNX Gemm node is defined as:
+		$Y = alpha * A * B + beta * C$
+
+		The translation defines the interactions:
+		$a_i ~ Mul(v_i, Concrete(alpha * b_i))$
+		$Add(...(Add(y_i, v_1), ...), v_n) ~ Concrete(beta * c_i)$
+
+		By definition this interaction is equal to:
+		$v_i = alpha * a_i * b_i$
+		$y_i = v_1 + v_2 + ... + v_n + beta * c_i$
+
+		By grouping the operations we get:
+		$Y = alpha * A * B + beta * C$
+
+*** Flatten
+		Just identity mapping.
+
+*** MatMul
+		Equal to Gemm with $alpha=1$ and $beta=0$.
+
+*** Reshape
+		Just identity mapping.
+
+** Soundness of Interaction Rules
+*** Materialize
+		The Materialize agent transforms a Linear agent into a tree of explicit mathematical operations
+		that are used as final representation for the solver.
+		In the Python module the terms are defined as:
+		@code python
 		def TermAdd(a, b):
 			return a + b  
 		def TermMul(a, b):
@@ -68,396 +69,415 @@ version: 1.1.1
 		def TermReLU(x):
 			return z3.If(x > 0, x, 0)
 	@end
-*** Linear(x, q, r) >< Materialize(out) => (1), (2), (3), (4), (5)
-		LHS:
-		Linear(x, q, r) ~ wire
-		Materialize(out) ~ wire
-		q*x + r = wire
-		out = wire
-		out = q*x + r
-
-		$$ Case 1: q = 0 => out ~ Concrete(r), x ~ Eraser
-		RHS:
-		out = r
-
-		EQUIVALENCE:
-		0*x + r = r => r = r
-		$$
-
-		$$ Case 2: q = 1, r = 0 => out ~ x
-		RHS:
-		x = out
-		out = x
-
-		EQUIVALENCE:
-		1*x + 0 = x => x = x
-		$$
-
-		$$ Case 3: q = 1 => out ~ TermAdd(x, Concrete(r))
-		RHS:
-		out = x + r
-
-		EQUIVALENCE:
-		1*x + r = x + r => x + r = x + r
-		$$
-
-		$$ Case 4: r = 0 => out ~ TermMul(Concrete(q), x)
-		RHS:
-		out = q*x
-
-		EQUIVALENCE:
-		q*x + 0 = q*x => q*x = q*x
-		$$
-
-		$$ Case 5: otherwise => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r))
-		RHS:
-		out = q*x + r
-
-		EQUIVALENCE:
-		q*x + r = q*x + r
-		$$
-
-*** Concrete(k) >< Materialize(out) => out ~ Concrete(k)
-		LHS:
-		Concrete(k) ~ wire
-		Materialize(out) ~ wire
-		k = wire
-		out = wire
-		out = k
-
-		RHS:
-		out = k
-
-		EQUIVALENCE:
-		k = k
-
-** Add
-*** Linear(x, q, r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r)
-		LHS:
-		Linear(x, q, r) ~ wire
-		Add(out, b) ~ wire
-		q*x + r = wire
-		out = wire + b
-		out = q*x + r + b
-
-		RHS:
-		out = q*x + (r + b)
-
-		EQUIVALENCE:
-		q*x + r + b = q*x + (r + b) => q*x + (r + b) = q*x + (r + b)
-
-*** Concrete(k) >< Add(out, b) => (1), (2)
-		LHS:
-		Concrete(k) ~ wire
-		Add(out, b) ~ wire
-		k = wire
-		out = wire + b
-		out = k + b
-
-		$$ Case 1: k = 0 => out ~ b
-		RHS:
-		out = b
-
-		EQUIVALENCE:
-		0 + b = b => b = b
-		$$
-
-		$$ Case 2: otherwise => b ~ AddCheckConcrete(out, k)
-		RHS:
-		out = k + b
-
-		EQUIVALENCE:
-		k + b = k + b
-		$$
-
-*** Linear(y, s, t) >< AddCheckLinear(out, x, q, r) => (1), (2), (3), (4)
-		LHS:
-		Linear(y, s, t) ~ wire
-		AddCheckLinear(out, x, q, r) ~ wire
-		s*y + t = wire
-		out = q*x + (r + wire)
-		out = q*x + (r + s*y + t)
-
-		$$ Case 1: q,r,s,t = 0 => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
-		RHS:
-		out = 0
-
-		EQUIVALENCE:
-		0*x + (0 + 0*y + 0) = 0 => 0 = 0
-		$$
-
-		$$ Case 2: s,t = 0 => out ~ Linear(x, q, r), y ~ Eraser
-		RHS:
-		out = q*x + r
-
-		EQUIVALENCE:
-		q*x + (r + 0*y + 0) = q*x + r => q*x + r = q*x + r
-		$$
-
-		$$ Case 3: q, r = 0 => out ~ Linear(y, s, t), x ~ Eraser
-		RHS:
-		out = s*y + t
-
-		EQUIVALENCE:
-		0*x + (0 + s*y + t) = s*y + t => s*y + t = s*y + t
-		$$
-
-		$$ Case 4: otherwise => Linear(x, q, r) ~ Materialize(out_x), Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0)
-		RHS:
-		Linear(x, q, r) ~ wire1
-		Materialize(out_x) ~ wire1
-		q*x + r = wire1
-		out_x = wire1
-		Linear(y, s, t) ~ wire2
-		Materialize(out_y) ~ wire2
-		s*y + t = wire2
-		out_y = wire2
-		out = 1*TermAdd(out_x, out_y) + 0
-		Because TermAdd(a, b) is defined as "a+b":
-		out = 1*(q*x + r + s*y + t) + 0
-
-		EQUIVALENCE:
-		q*x + (r + s*y + t) = 1*(q*x + r + s*y + t) + 0 => q*x + r + s*y + t = q*x + r + s*y + t
-		$$
-
-*** Concrete(j) >< AddCheckLinear(out, x, q, r) => out ~ Linear(x, q, r + j)
-		LHS:
-		Concrete(j) ~ wire
-		AddCheckLinear(out, x, q, r) ~ wire
-		j = wire
-		out = q*x + (r + wire)
-		out = q*x + (r + j)
-
-		RHS:
-		out = q*x + (r + j)
-
-		EQUIVALENCE:
-		q*x + (r + j) = q*x + (r + j)
-
-*** Linear(y, s, t) >< AddCheckConcrete(out, k) => out ~ Linear(y, s, t + k)
-		LHS:
-		Linear(y, s, t) ~ wire
-		AddCheckConcrete(out, k) ~ wire
-		s*y + t = wire
-		out = k + wire
-		out = k + s*y + t
-
-		RHS:
-		out = s*y + (t + k)
-
-		EQUIVALENCE:
-		k + s*y + t = s*y + (t + k) => s*y + (t + k) = s*y + (t + k)
-
-*** Concrete(j) >< AddCheckConcrete(out, k) => (1), (2)
-		LHS:
-		Concrete(j) ~ wire
-		AddCheckConcrete(out, k) ~ wire
-		j = wire
-		out = k + wire
-		out = k + j
-
-		$$ Case 1: j = 0 => out ~ Concrete(k)
-		RHS:
-		out = k
-
-		EQUIVALENCE:
-		k + 0 = k => k = k
-		$$
-
-		$$ Case 2: otherwise => out ~ Concrete(k + j)
-		RHS:
-		out = k + j
-
-		EQUIVALENCE:
-		k + j = k + j
-		$$
-
-** Mul
-*** Linear(x, q, r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r)
-		LHS:
-		Linear(x, q, r) ~ wire
-		Mul(out, b) ~ wire
-		q*x + r = wire
-		out = wire * b
-		out = (q*x + r) * b
-
-		RHS:
-		out = q*b*x + r*b
-
-		EQUIVALENCE:
-		(q*x + r) * b = q*b*x + r*b => q*b*x + r*b = q*b*x + r*b
-
-*** Concrete(k) >< Mul(out, b) => (1), (2), (3)
-		LHS:
-		Concrete(k) ~ wire
-		Mul(out, b) ~ wire
-		k = wire
-		out = wire * b
-		out = k * b
-
-		$$ Case 1: k = 0 => out ~ Concrete(0), b ~ Eraser
-		RHS:
-		out = 0
-
-		EQUIVALENCE:
-		0 * b = 0 => 0 = 0
-		$$
-
-		$$ Case 2: k = 1 => out ~ b
-		RHS:
-		out = b
-
-		EQUIVALENCE:
-		1 * b = b => b = b
-		$$
-
-		$$ Case 3: otherwise => b ~ MulCheckConcrete(out, k)
-		RHS:
-		out = k * b
-
-		EQUIVALENCE:
-		k * b = k * b
-		$$
-
-*** Linear(y, s, t) >< MulCheckLinear(out, x, q, r) => (1), (2)
-		LHS:
-		Linear(y, s, t) ~ wire
-		MulCheckLinear(out, x, q, r) ~ wire
-		s*y + t = wire
-		out = q*wire*x + r*wire
-		out = q\*(s*y + t)\*x + r*(s*y + t)
-
-		$$ Case 1: (q,r = 0) or (s,t = 0) => x ~ Eraser, y ~ Eraser, out ~ Concrete(0)
-		RHS:
-		out = 0
-
-		EQUIVALENCE:
-		0\*(s*y + t)\*x + 0*(s*y + t) = 0 => 0 = 0
-		or
-		q\*(0*y + 0)\*x + r*(0*y + 0) = 0 => 0 = 0
-		$$
-
-		$$ Case 2: otherwise => Linear(x, q, r) ~ Materialize(out_x), Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0)
-		RHS:
-		Linear(x, q, r) ~ wire1
-		Materialize(out_x) ~ wire1
-		q*x + r = wire1
-		out_x = wire1
-		Linear(y, s, t) ~ wire2
-		Materialize(out_y) ~ wire2
-		s*y + t = wire2
-		out_y = wire2
-		out = 1*TermMul(out_x, out_y) + 0
-		Because TermMul(a, b) is defined as "a*b":
-		out = 1*(q*x + r)*(s*y + t) + 0
-
-		EQUIVALENCE:
-		q*(s*y + t)\*x + r*(s*y + t) = 1*(q*x + r)\*(s*y + t) => 
-		q\*(s*y + t)\*x + r*(s*y + t) = (q*x + r)\*(s*y + t) => 
-		q\*(s*y + t)\*x + r*(s*y + t) = q\*(s*y + t)\*x + r*(s*y + t)
-		$$
-
-*** Concrete(j) >< MulCheckLinear(out, x, q, r) => out ~ Linear(x, q * j, r * j)
-		LHS:
-		Concrete(j) ~ wire
-		MulCheckLinear(out, x, q, r) ~ wire
-		j = wire
-		out = q*wire*x + r*wire
-		out = q*j*x + r*j
-
-		RHS:
-		out = q*j*x + r*j
-
-		EQUIVALENCE:
-		q*j*x + r*j = q*j*x + r*j
-
-*** Linear(y, s, t) >< MulCheckConcrete(out, k) => out ~ Linear(y, s * k, t * k)
-		LHS:
-		Linear(y, s, t) ~ wire
-		MulCheckConcrete(out, k) ~ wire
-		s*y + t = wire
-		out = k * wire
-		out = k * (s*y + t)
-
-		RHS:
-		out = s*k*y + t*k
-
-		EQUIVALENCE:
-		k * (s*y + t) = s*k*y + t*k => s*k*y + t*k = s*k*y + t*k
-
-*** Concrete(j) >< MulCheckConcrete(out, k) => (1), (2), (3)
-		LHS:
-		Concrete(j) ~ wire
-		MulCheckConcrete(out, k) ~ wire
-		j = wire
-		out = k * wire
-		out = k * j
-
-		$$ Case 1: j = 0 => out ~ Concrete(0)
-		RHS:
-		out = 0
-
-		EQUIVALENCE:
-		k * 0 = 0 => 0 = 0
-		$$
-
-		$$ Case 2: j = 1 => out ~ Concrete(k)
-		RHS:
-		out = k
-
-		EQUIVALENCE:
-		k * 1 = k => k = k
-		$$
-
-		$$ Case 3: otherwise => out ~ Concrete(k * j)
-		RHS:
-		out = k * j
-
-		EQUIVALENCE:
-		k * j = k * j
-
-** ReLU
-*** Linear(x, q, r) >< ReLU(out) => Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0)
-		LHS:
-		Linear(x, q, r) ~ wire
-		ReLU(out) ~ wire
-		q*x + r = wire
-		out = IF wire > 0 THEN wire ELSE 0
-		out = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0
-
-		RHS:
-		Linear(x, q, r) ~ wire
-		Materialize(out_x) ~ wire
-		q*x + r = wire
-		out_x = wire
-		out = 1*TermReLU(out_x) + 0
-		Because TermReLU(x) is defined as "z3.If(x > 0, x, 0)":
-		out = 1*(IF (q*x + r) > 0 THEN (q*x + r) ELSE 0) + 0
-
-		EQUIVALENCE:
-		IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 = 1*(IF (q*x + r) > 0 THEN (q*x + r) ELSE 0) + 0 =>
-		IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0
-
-*** Concrete(k) >< ReLU(out) => (1), (2)
-		LHS:
-		Concrete(k) ~ wire
-		ReLU(out) ~ wire
-		k = wire
-		out = IF wire > 0 THEN wire ELSE 0
-		out = IF k > 0 THEN k ELSE 0
-
-		$$ Case 1: k > 0 => out ~ Concrete(k)
-		RHS:
-		out = k
-
-		EQUIVALENCE:
-		IF true THEN k ELSE 0 = k => k = k
-		$$
-
-		$$ Case 2: k <= 0 => out ~ Concrete(0)
-		RHS:
-		out = 0
-
-		EQUIVALENCE:
-		IF false THEN k ELSE 0 = 0 => 0 = 0
-		$$
+**** $Linear(x, q, r) >< Materialize(out) => (1), (2), (3), (4), (5)$
+		 LHS:
+		 $Linear(x, q, r) ~ wire$
+		 $Materialize(out) ~ wire$
+		 $q*x + r = wire$
+		 $out = wire$
+		 $out = q*x + r$
+
+		 $$ Case 1: $q = 0 => out ~ Concrete(r), x ~ Eraser$
+		 RHS:
+		 $out = r$
+
+		 EQUIVALENCE:
+		 $0*x + r = r => r = r$
+		 $$
+
+		 $$ Case 2: $q = 1, r = 0 => out ~ x$
+		 RHS:
+		 $x = out$
+		 $out = x$
+
+		 EQUIVALENCE:
+		 $1*x + 0 = x => x = x$
+		 $$
+
+		 $$ Case 3: $q = 1 => out ~ TermAdd(x, Concrete(r))$
+		 RHS:
+		 $out = x + r$
+
+		 EQUIVALENCE:
+		 $1*x + r = x + r => x + r = x + r$
+		 $$
+
+		 $$ Case 4: $r = 0 => out ~ TermMul(Concrete(q), x)$
+		 RHS:
+		 $out = q*x$
+
+		 EQUIVALENCE:
+		 $q*x + 0 = q*x => q*x = q*x$
+		 $$
+
+		 $$ Case 5: $otherwise => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r))$
+		 RHS:
+		 $out = q*x + r$
+
+		 EQUIVALENCE:
+		 $q*x + r = q*x + r$
+		 $$
+
+**** $Concrete(k) >< Materialize(out) => out ~ Concrete(k)$
+		 LHS:
+		 $Concrete(k) ~ wire$
+		 $Materialize(out) ~ wire$
+		 $k = wire$
+		 $out = wire$
+		 $out = k$
+
+		 RHS:
+		 $out = k$
+
+		 EQUIVALENCE:
+		 $k = k$
+
+*** Add
+**** $Linear(x, q, r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r)$
+		 LHS:
+		 $Linear(x, q, r) ~ wire$
+		 $Add(out, b) ~ wire$
+		 $q*x + r = wire$
+		 $out = wire + b$
+		 $out = q*x + r + b$
+
+		 RHS:
+		 $out = q*x + (r + b)$
+
+		 EQUIVALENCE:
+		 $q*x + r + b = q*x + (r + b) => q*x + (r + b) = q*x + (r + b)$
+
+**** $Concrete(k) >< Add(out, b) => (1), (2)$
+		 LHS:
+		 $Concrete(k) ~ wire$
+		 $Add(out, b) ~ wire$
+		 $k = wire$
+		 $out = wire + b$
+		 $out = k + b$
+
+		 $$ Case 1: $k = 0 => out ~ b$
+		 RHS:
+		 $out = b$
+
+		 EQUIVALENCE:
+		 $0 + b = b => b = b$
+		 $$
+
+		 $$ Case 2: $otherwise => b ~ AddCheckConcrete(out, k)$
+		 RHS:
+		 $out = k + b$
+
+		 EQUIVALENCE:
+		 $k + b = k + b$
+		 $$
+
+**** $Linear(y, s, t) >< AddCheckLinear(out, x, q, r) => (1), (2), (3), (4)$
+		 LHS:
+		 $Linear(y, s, t) ~ wire$
+		 $AddCheckLinear(out, x, q, r) ~ wire$
+		 $s*y + t = wire$
+		 $out = q*x + (r + wire)$
+		 $out = q*x + (r + s*y + t)$
+
+		 $$ Case 1: $q,r,s,t = 0 => out ~ Concrete(0), x ~ Eraser, y ~ Eraser$
+		 RHS:
+		 $out = 0$
+
+		 EQUIVALENCE:
+		 $0*x + (0 + 0*y + 0) = 0 => 0 = 0$
+		 $$
+
+		 $$ Case 2: $s,t = 0 => out ~ Linear(x, q, r), y ~ Eraser$
+		 RHS:
+		 $out = q*x + r$
+
+		 EQUIVALENCE:
+		 $q*x + (r + 0*y + 0) = q*x + r => q*x + r = q*x + r$
+		 $$
+
+		 $$ Case 3: $q, r = 0 => out ~ Linear(y, s, t), x ~ Eraser$
+		 RHS:
+		 $out = s*y + t$
+
+		 EQUIVALENCE:
+		 $0*x + (0 + s*y + t) = s*y + t => s*y + t = s*y + t$
+		 $$
+
+		 $$ Case 4: $otherwise => Linear(x, q, r) ~ Materialize(out_x), Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0)$
+		 RHS:
+		 $Linear(x, q, r) ~ wire1$
+		 $Materialize(out_x) ~ wire1$
+		 $q*x + r = wire1$
+		 $out_x = wire1$
+		 $Linear(y, s, t) ~ wire2$
+		 $Materialize(out_y) ~ wire2$
+		 $s*y + t = wire2$
+		 $out_y = wire2$
+		 $out = 1*TermAdd(out_x, out_y) + 0$
+		 Because $TermAdd(a, b)$ is defined as "a+b$:
+		 $out = 1*(q*x + r + s*y + t) + 0$
+
+		 EQUIVALENCE:
+		 $q*x + (r + s*y + t) = 1*(q*x + r + s*y + t) + 0 => q*x + r + s*y + t = q*x + r + s*y + t
+		 $$
+
+**** $Concrete(j) >< AddCheckLinear(out, x, q, r) => out ~ Linear(x, q, r + j)$
+		 LHS:
+		 $Concrete(j) ~ wire$
+		 $AddCheckLinear(out, x, q, r) ~ wire$
+		 $j = wire$
+		 $out = q*x + (r + wire)$
+		 $out = q*x + (r + j)$
+
+		 RHS:
+		 $out = q*x + (r + j)$
+
+		 EQUIVALENCE:
+		 $q*x + (r + j) = q*x + (r + j)$
+
+**** $Linear(y, s, t) >< AddCheckConcrete(out, k) => out ~ Linear(y, s, t + k)$
+		 LHS:
+		 $Linear(y, s, t) ~ wire$
+		 $AddCheckConcrete(out, k) ~ wire$
+		 $s*y + t = wire$
+		 $out = k + wire$
+		 $out = k + s*y + t$
+
+		 RHS:
+		 $out = s*y + (t + k)$
+
+		 EQUIVALENCE:
+		 $k + s*y + t = s*y + (t + k) => s*y + (t + k) = s*y + (t + k)$
+
+**** $Concrete(j) >< AddCheckConcrete(out, k) => (1), (2)$
+		 LHS:
+		 $Concrete(j) ~ wire$
+		 $AddCheckConcrete(out, k) ~ wire$
+		 $j = wire$
+		 $out = k + wire$
+		 $out = k + j$
+
+		 $$ Case 1: $j = 0 => out ~ Concrete(k)$
+		 RHS:
+		 $out = k$
+
+		 EQUIVALENCE:
+		 $k + 0 = k => k = k$
+		 $$
+
+		 $$ Case 2: $otherwise => out ~ Concrete(k + j)$
+		 RHS:
+		 $out = k + j$
+
+		 EQUIVALENCE:
+		 $k + j = k + j$
+		 $$
+
+*** Mul
+**** $Linear(x, q, r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r)$
+		 LHS:
+		 $Linear(x, q, r) ~ wire$
+		 $Mul(out, b) ~ wire$
+		 $q*x + r = wire$
+		 $out = wire * b$
+		 $out = (q*x + r) * b$
+
+		 RHS:
+		 $out = q*b*x + r*b$
+
+		 EQUIVALENCE:
+		 $(q*x + r) * b = q*b*x + r*b => q*b*x + r*b = q*b*x + r*b$
+
+**** $Concrete(k) >< Mul(out, b) => (1), (2), (3)$
+		 LHS:
+		 $Concrete(k) ~ wire$
+		 $Mul(out, b) ~ wire$
+		 $k = wire$
+		 $out = wire * b$
+		 $out = k * b$
+
+		 $$ Case 1: $k = 0 => out ~ Concrete(0), b ~ Eraser$
+		 RHS:
+		 $out = 0$
+
+		 EQUIVALENCE:
+		 $0 * b = 0 => 0 = 0$
+		 $$
+
+		 $$ Case 2: $k = 1 => out ~ b$
+		 RHS:
+		 $out = b$
+
+		 EQUIVALENCE:
+		 $1 * b = b => b = b$
+		 $$
+
+		 $$ Case 3: $otherwise => b ~ MulCheckConcrete(out, k)$
+		 RHS:
+		 $out = k * b$
+
+		 EQUIVALENCE:
+		 $k * b = k * b$
+		 $$
+
+**** $Linear(y, s, t) >< MulCheckLinear(out, x, q, r) => (1), (2)$
+		 LHS:
+		 $Linear(y, s, t) ~ wire$
+		 $MulCheckLinear(out, x, q, r) ~ wire$
+		 $s*y + t = wire$
+		 $out = q*wire*x + r*wire$
+		 $out = q*(s*y + t)*x + r*(s*y + t)$
+
+		 $$ Case 1: $(q,r = 0) or (s,t = 0) => x ~ Eraser, y ~ Eraser, out ~ Concrete(0)$
+		 RHS:
+		 $out = 0$
+
+		 EQUIVALENCE:
+		 $0*(s*y + t)*x + 0*(s*y + t) = 0 => 0 = 0$
+		 or
+		 $q*(0*y + 0)*x + r*(0*y + 0) = 0 => 0 = 0$
+		 $$
+
+		 $$ Case 2: $otherwise => Linear(x, q, r) ~ Materialize(out_x), Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0)$
+		 RHS:
+		 $Linear(x, q, r) ~ wire1$
+		 $Materialize(out_x) ~ wire1$
+		 $q*x + r = wire1$
+		 $out_x = wire1$
+		 $Linear(y, s, t) ~ wire2$
+		 $Materialize(out_y) ~ wire2$
+		 $s*y + t = wire2$
+		 $out_y = wire2$
+		 $out = 1*TermMul(out_x, out_y) + 0$
+		 Because $TermMul(a, b)$ is defined as $a*b$:
+		 $out = 1*(q*x + r)*(s*y + t) + 0$
+
+		 EQUIVALENCE:
+		 $q*(s*y + t)*x + r*(s*y + t) = 1*(q*x + r)*(s*y + t) => 
+		 q*(s*y + t)*x + r*(s*y + t) = (q*x + r)*(s*y + t) => 
+		 q*(s*y + t)*x + r*(s*y + t) = q*(s*y + t)*x + r*(s*y + t)$
+		 $$
+
+**** $Concrete(j) >< MulCheckLinear(out, x, q, r) => out ~ Linear(x, q * j, r * j)$
+		 LHS:
+		 $Concrete(j) ~ wire$
+		 $MulCheckLinear(out, x, q, r) ~ wire$
+		 $j = wire$
+		 $out = q*wire*x + r*wire$
+		 $out = q*j*x + r*j$
+
+		 RHS:
+		 $out = q*j*x + r*j$
+
+		 EQUIVALENCE:
+		 $q*j*x + r*j = q*j*x + r*j$
+
+**** $Linear(y, s, t) >< MulCheckConcrete(out, k) => out ~ Linear(y, s * k, t * k)$
+		 LHS:
+		 $Linear(y, s, t) ~ wire$
+		 $MulCheckConcrete(out, k) ~ wire$
+		 $s*y + t = wire$
+		 $out = k * wire$
+		 $out = k * (s*y + t)$
+
+		 RHS:
+		 $out = s*k*y + t*k$
+
+		 EQUIVALENCE:
+		 $k * (s*y + t) = s*k*y + t*k => s*k*y + t*k = s*k*y + t*k$
+
+**** $Concrete(j) >< MulCheckConcrete(out, k) => (1), (2), (3)$
+		 LHS:
+		 $Concrete(j) ~ wire$
+		 $MulCheckConcrete(out, k) ~ wire$
+		 $j = wire$
+		 $out = k * wire$
+		 $out = k * j$
+
+		 $$ Case 1: $j = 0 => out ~ Concrete(0)$
+		 RHS:
+		 $out = 0$
+
+		 EQUIVALENCE:
+		 $k * 0 = 0 => 0 = 0$
+		 $$
+
+		 $$ Case 2: $j = 1 => out ~ Concrete(k)$
+		 RHS:
+		 $out = k$
+
+		 EQUIVALENCE:
+		 $k * 1 = k => k = k$
+		 $$
+
+		 $$ Case 3: $otherwise => out ~ Concrete(k * j)$
+		 RHS:
+		 $out = k * j$
+
+		 EQUIVALENCE:
+		 $k * j = k * j$
+
+*** ReLU
+**** $Linear(x, q, r) >< ReLU(out) => Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0)$
+		 LHS:
+		 $Linear(x, q, r) ~ wire$
+		 $ReLU(out) ~ wire$
+		 $q*x + r = wire$
+		 $out = IF wire > 0 THEN wire ELSE 0$
+		 $out = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0$
+
+		 RHS:
+		 $Linear(x, q, r) ~ wire$
+		 $Materialize(out_x) ~ wire$
+		 $q*x + r = wire$
+		 $out_x = wire$
+		 $out = 1*TermReLU(out_x) + 0$
+		 Because $TermReLU(x)$ is defined as $z3.If(x > 0, x, 0)$:
+		 $out = 1*(IF (q*x + r) > 0 THEN (q*x + r) ELSE 0) + 0$
+
+		 EQUIVALENCE:
+		 $IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 = 1*(IF (q*x + r) > 0 THEN (q*x + r) ELSE 0) + 0 =>
+		 IF (q*x + r) > 0 THEN (q*x + r) ELSE 0 = IF (q*x + r) > 0 THEN (q*x + r) ELSE 0$
+
+**** $Concrete(k) >< ReLU(out) => (1), (2)$
+		 LHS:
+		 $Concrete(k) ~ wire$
+		 $ReLU(out) ~ wire$
+		 $k = wire$
+		 $out = IF wire > 0 THEN wire ELSE 0$
+		 $out = IF k > 0 THEN k ELSE 0$
+
+		 $$ Case 1: $k > 0 => out ~ Concrete(k)$
+		 RHS:
+		 $out = k$
+
+		 EQUIVALENCE:
+		 $IF true THEN k ELSE 0 = k => k = k$
+		 $$
+
+		 $$ Case 2: $k <= 0 => out ~ Concrete(0)$
+		 RHS:
+		 $out = 0$
+
+		 EQUIVALENCE:
+		 $IF false THEN k ELSE 0 = 0 => 0 = 0$
+		 $$
+
+** Soundness of Reduction 
+	 Let $IN_0$ be the Interaction Net translated from a Neural Network $NN$. Let $IN_n$ be the state of the net
+	 after $n$ reduction steps. Then $\forall n \in N$, $[IN_n] = [NN]$.
+
+*** Proof by Induction
+		- Base Case ($n = 0$): By the {* Soundness of Translation}, the initial net $IN_0$ is constructed such that
+			its semantics $[IN_0]$ exactly match the mathematical definition of the ONNX nodes in $NN$.
+		- Induction Step ($n -> n + 1$): Assume $[IN_n] = [NN]$. If $IN_n$ is in normal form, the proof is complete.
+			Otherwise, there exists an active pair $A$ that reduces $IN_n$ to $IN_{n+1}$.
+			By the {* Soundness of Interaction Rules}, the mathematical definition is preserved after any reduction step,
+		it follows that $[IN_{n+1}] = [IN_n]$. By the inductive hypothesis, $[IN_{n+1}] = [NN]$.
+		---
+
+	 By the principle of mathematical induction, the Interaction Net remains semantically equivalent to the original 
+	 Neural Network at every step of the reduction process.
+
+	 Since Interaction Nets are confluent, the reduced mathematical expression is unique regardless
+	 of order in which rules are applied.