From 81d4d604aa43660b732b3538734a52d509d7c5df Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Tue, 31 Mar 2026 16:43:47 +0200
Subject: refactored examples

---
 proof.norg | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'proof.norg')

diff --git a/proof.norg b/proof.norg
index 36851a9..7bd9e25 100644
--- a/proof.norg
+++ b/proof.norg
@@ -48,13 +48,15 @@ version: 1.1.1
 		$Y = alpha * A * B + beta * C$
 
 *** Flatten
-		Just identity mapping.
+		Just identity mapping because the wires are always Flatten.
+		$o_i ~ i_i$
 
 *** MatMul
-		Equal to Gemm with $alpha=1$ and $beta=0$.
+		Equal to Gemm with $alpha=1$, $beta=0$ and $C=0$.
 
 *** Reshape
-		Just identity mapping.
+		Just identity mapping because the wires always Flatten.
+		$o_i ~ i_i$
 
 *** Add
 		ONNX Add node is defined as:
@@ -491,7 +493,7 @@ version: 1.1.1
 		 $IF false THEN k ELSE 0 = 0 => 0 = 0$
 		 $$
 
-** Soundness of Reduction 
+** 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]$.
 
-- 
cgit v1.2.3