From d1b25fbde6b01529fd1bcfdd5778b6cb378eb865 Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Tue, 31 Mar 2026 11:14:57 +0200
Subject: added ONNX Add and ONNX Sub

---
 proof.norg | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'proof.norg')

diff --git a/proof.norg b/proof.norg
index 21f1fcd..36851a9 100644
--- a/proof.norg
+++ b/proof.norg
@@ -56,6 +56,34 @@ version: 1.1.1
 *** Reshape
 		Just identity mapping.
 
+*** Add
+		ONNX Add node is defined as:
+		$C = A + B$
+
+		The translation defines the interactions:
+		$Add(c_i, b_i) ~ a_i$
+
+		By definition this interaction is equal to:
+		$c_i = a_i + b_i$
+
+		By grouping the operations we get:
+		$C = A + B$
+
+*** Sub
+		ONNX Sub node is defined as:
+		$C = A - B$
+
+		The translation defines the interactions:
+		$Add(c_i, neg_b_i) ~ a_i$
+		$Mul(neg_b_i, Concrete(-1)) ~ b_i$
+
+		By definition this interaction is equal to:
+		$c_i = a_i + neg_b_i$
+		$neg_b_i = -1 * b_i$
+
+		By grouping the operations we get:
+		$C = A - B$
+
 ** Soundness of Interaction Rules
 *** Materialize
 		The Materialize agent transforms a Linear agent into a tree of explicit mathematical operations
-- 
cgit v1.2.3