defined modules

10 files changed, 1253 insertions, 461 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..930f082
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/nneq/__pycache__
diff --git a/Gentle_introduction_Inpla.md b/Gentle_introduction_Inpla.md
new file mode 100644
index 0000000..5156e31
--- /dev/null
+++ b/Gentle_introduction_Inpla.md
@@ -0,0 +1,899 @@
+# Gentle introduction to Inpla
+#### Contents in this section
+* [Nets: terms and connections](#nets-terms-and-connections)
+* [Interaction rules: rewriting rules for nets](#interaction-rules-rewriting-rules-for-nets)
+  - [Example: Operations on unary natural numbers](#example-operations-on-unary-natural-numbers)
+  - [Abbreviation notation `<<`](#abbreviation-notation-)
+* [Built-in Agents](#built-in-agents)
+  - [Tuples](#tuples)
+  - [Lists](#lists)
+  - [Built-in rules for tuples and lists](#built-in-rules-for-tuples-and-lists)
+* [Attributes (integers)](#attributes-integers)
+  - [Built-in anonymous agent for attributes](#built-in-anonymous-agent-for-attributes)
+  - [Arithmetic expressions on attributes](#arithmetic-expressions-on-attributes)
+  - [Interaction rules with expressions on attributes](#interaction-rules-with-expressions-on-attributes)
+  - [Built-in rules of attributes in the anonymous agents](#built-in-rules-of-attributes-in-the-anonymous-agents)
+  - [Interaction rules with conditions on attributes](#interaction-rules-with-conditions-on-attributes)
+* [Commands](#commands)
+* [Execution Options](#execution-options)
+* [Advanced topics](#advanced-topics)
+  * [Wildcard agent in rule definitions](#Wildcard-agent-in-rule-definitions)
+  * [Reuse annotations](#reuse-annotations)
+  * [built-in agents more](#built-in-agents-more)
+  * [Map and reduce functions (with Abbreviation notation `%`)](#map-and-reduce-functions)
+  * [Weak reduction strategy](#weak-reduction-strategy)
+
+
+
+
+## Nets: terms and connections
+
+Inpla evaluates *nets*, which are built by *connections between terms*. First, we start learning about terms and connections.
+
+### Terms
+
+**Terms** are built on *names* and *agents* as follows:
+
+```
+<term> ::= <name> | <agent>
+<name> ::= <nameID>
+<agent> ::= <agentID>
+          | <agentID> ['(' <term> ',' ... ',' <term> ')']     
+```
+* **Name**: It works as a buffer between terms. The ```<nameID>``` is defined as strings start with a small letter, e.g. ```x``` and ```y```. To show connected terms from names, type the names. For instance, type just `x` to show a term connected from the 'x':
+
+  ```
+  >>> x;
+  <NON-DEFINED>
+  >>>
+  ```
+
+  The above execution means that nothing has been connected from the `x` yet, of course.
+  We have **Linearity restriction** for names such that **each name must occur at most twice**. This is required in order to ensure one-to-one connections between terms.
+
+* **Agent**: It works as a constructor and de-constructor (defined functions). Generally agents have one *principal port* and *n*-fixed *auxiliary ports*. The fixed number of auxiliary ports is called *arity*, and it is determined according to each agent sort. In graphical representation an agent term `A(x1,...,xn)`, whose arity is *n*, is drawn as the following picture, where its auxiliary ports and the principal port (drawn as an arrow) correspond to the occurrences of the `x1`,...`xn`, and `A(x1,...,xn)`, respectively: 
+  
+  ![agent](pic/agent.png)
+  
+  The ```<agentID>``` is defined as strings start with a capital letter, e.g. ```A``` and ```Succ```, and also ```<nameID>``` followed by a open curry bracket```(```. So, ```foo(x)``` is recognised as an agent. 
+
+  
+
+### Connections
+
+A **connection** is a relation between two terms, that means the two term are connected, and it is expressed with the symbol `~`. For instance, a connection between a name `x` and an agent `A` (whose arity is 0) is denoted as `x~A`. There is no order in the left-hand and the right-hand side terms, thus `x~A` and `A~x` are identified as the same one.
+
+* **Connections between a name and an agent** are evaluated as that the agent is connected from the name. For instance, `x~A` is evaluated as that the `A` is connected from the `x`.   Here, as an example, type `x~A` with the termination symbol `;` as follows:
+  
+  ```
+  >>> x~A;
+  (0 interactions, 0.00 sec)
+  >>>
+  ```
+  
+  To show the connected terms from the name x, type just `x`:  
+  ```
+  >>> x;
+  A
+  >>>
+  ```
+  
+  To dispose the name `x` and anything connected from the `x`, use `free` command:
+  ```
+  >>> free x;
+  >>> x;
+  <NON-DEFINED>
+  >>>
+  ```
+
+
+* **Connections between names** are evaluated as that ports corresponding to these names are connected mutually in interaction nets frameworks. However, in Inpla, these are evaluated as that, for the connections, the left-hand side name connects to the right-hand side name, thus only one way. For instance, `x~y` is evaluated that the `x` connects to the `y` (not that the `y` connects to `x`):
+
+  ```
+  >>> x~y;
+  >>> x;
+  y
+  >>> y;
+  <EMPTY>
+  >>>
+  ```
+
+* **Connections between agents** are evaluated according to *interaction rules* explained later. 
+
+Two connections that have the same name at the right or left hand sides, say `t~x` and `x~s`, are written as `t~s`.  **We note** that the `x` is disposed after rewriting so that every connection can be kept one-to-one via names, cannot be one-to-many.
+```
+>>> x~A, x~y;
+(0 interactions, 0.00 sec)
+>>> y;
+A
+>>> x;        // x has been consumed by the re-connection of x~A and x~y.
+<NON-DEFINED>
+>>>
+```
+
+Just in case for other examples, let the `y` disposed:
+
+```
+>>> free y;
+>>> y;
+<NON-DEFINED>
+>>>
+```
+
+
+
+## Interaction rules: rewriting rules for nets
+
+Connections between agents are rewritten according to **interaction rules**:
+
+```
+<interaction-rule> ::= <rule-agent> '><' <rule-agent> '=>' <connections> ';'
+<rule-agent> ::= <agentID>
+               | <agentID> '(' <name> ',' ... ',' <name> ')'
+```
+  with the **proviso** that:
+
+  * each name that occur in the two `<rule-agent>` must be **distinct**
+  * (**Linearity restriction**): every name in the `<interaction-rule>` must **occur twice**.
+
+Something complicated? No problem! Let's us learn how to define the rules with some example!
+
+### Example: Operations on unary natural numbers
+
+Unary natural numbers are built by Z and S. For instance, 0, 1, 2, 3 are expressed as Z, S(Z), S(S(Z)), S(S(S(Z))). Here, let's think about an increment operation "inc" such that:
+```
+ inc(n) = S(n).
+```
+
+First, we will think about the relationship between constructors and deconstructors in  this computation.
+Here, constructors are agents `Z`, `S(x)`, and a destructor is `inc(r)` which has an argument for the output. The behaviour of `inc(r)` will be as follows:
+* When `inc(r)` meets `Z`, the output `r` is connected to `S(Z)`. 
+* In the case of `S(x)`, the `r` is connected to `S(S(x))`. 
+
+
+ This is written as the following rules:
+```
+inc(r) >< Z => r~S(Z);
+inc(r) >< S(x) => r~S(S(x));
+```
+
+Let's check the rule proviso. In the first rule, the name `r` occurs twice, so it satisfies the proviso. The second rule is also OK because the `r` and `x` are distinct and occur twice in the rule. 
+
+Since agents can work as both constructors and de-constructors, we should use capitalised strings such as `Z`, `S` and `Tree` for constructors, and lowercases for de-constructors such as `inc`.
+
+Let's take the result of the increment operation for `S(S(Z))`:
+
+```
+>>> inc(r) >< Z => r~S(Z);
+>>> inc(r) >< S(x) => r~S(S(x));
+>>> inc(r)~S(S(Z));
+(1 interactions, 0.01 sec)
+>>> r;
+S(S(S(Z))
+>>>
+```
+
+Good! We get `S(S(S(Z)))` as the result of incrementation of  `S(S(Z))` .
+
+To show the result as a natural number, use `prnat` command:
+
+```
+>>> prnat r;
+3
+>>>
+```
+
+Let's clean the result in case it could be used anywhere:
+
+```
+>>> free r;
+>>>
+```
+
+* **Exercise**: Addition on unary natural numbers.
+
+  It is defined recursively in term rewriting systems as follows:
+
+  - add(x, Z) = x,  
+  - add(x, S(y)) = add(S(x), y).
+  
+  This is written in interaction nets as follows: ![add1](pic/add1.png)
+  
+  In Inpla (and textual notation in interaction nets also), each agent is expressed as a term whose arguments correspond to its auxiliary ports. For instance, the `add` agent in the most left-hand side of the above figure, putting distinct names on auxiliary ports such as `ret` and `x`, is written as a term `add(ret,x)` by assembling these names anti-clockwise from the principal port (drawn as an arrow). 
+  
+  Every computation is performed on connections between principal ports according to interaction rules. The rules shown in above figure are written textually as follows:
+  
+  ```
+  add(ret, x) >< Z => ret~x;
+  add(ret, x) >< S(y) => add(ret, S(x))~y;
+  ```
+  The following is an execution example:
+  ```
+  >>> add(ret, x) >< Z => ret~x;
+  >>> add(ret, x) >< S(y) => add(ret, S(x))~y;
+  >>> add(r,S(Z))~S(S(Z));
+  (2 interactions, 0.00 sec)
+  >>> r;
+  S(S(S(Z)))
+  >>> prnat r;
+  3
+  >>> free r;
+  >>>
+  ```
+  
+* **Exercise**: Another version of the addition.
+
+  There is another version as follows:
+
+  - add(x,Z) = x,
+  - add(x, S(y)) = S(add(x,y)).
+
+  These are written in interaction nets: ![add2](pic/add2.png)
+  
+  and written textually as follows:
+  
+  ```
+  add(ret,x) >< Z => ret~x;
+  add(ret,x) >< S(y) => ret~S(cnt), add(cnt, x)~y;
+  ```
+  In comparison with the previous example, calculation results can be sent partially as `S(cnt)` to other soon, whereas those in the previous one are stored until all of computation finish. So, **this version is suitable for parallel execution**.
+  
+  
+### Abbreviation notation `<<`: 
+An abbreviation notation `<<` is defined as follows:
+```
+a,b,...,z << Agent(aa,bb,...,yy,zz)   == for ==  Agent(a,b,...,z,aa,bb,...,yy) ~ zz 
+```
+For instance, `r << add(S(Z),S(S(Z)))` is rewritten internally as `add(r,S(Z))~S(S(Z))`. It is handy to denote ports that take computation results.
+
+
+## Built-in Agents
+Inpla has built-in agents:
+
+### Tuples
+
+* `Tuple0`,  `Tuple2(x1,x2)`,  `Tuple3(x1,x2,x2)`,  `Tuple4(x1,x2,x3,x4)`,  `Tuple5(x1,x2,x3,x4,x5)`,   written as   `()`,  `(x1,x2)`,  `(x1,x2,x3)`, `(x1,x2,x3,x4)`, `(x1,x2,x3,x4,x5)`, respectively.
+  
+* There is no Tuple1. `(x)` is evaluated just as `x`.
+
+
+### Lists
+
+* `Nil`, `Cons(x,xs)`, written as  `[]` and `x:xs`, respectively. 
+* A nested `Cons` terminated with `Nil` are written as a list notation using brackets `[` and `]`.  For instance,  `x1 : x2: x3 : Nil`  is written as  `[x1,x2,x3]` .  
+
+### Built-in rules for tuples and lists
+
+There are built-in rules for the same built-in agents that each element is matched and connected such that:
+
+```
+(x1,x2)><(y1,y2) => x1~y1, x2~y2 // This is already defined as a built-in rule.
+```
+
+* Examples of the built-in rules:
+
+  ```
+  >>> (x1,x2)~(Z, S(Z));
+  (1 interactions, 0.00 sec)
+  >>> x1 x2;
+  Z S(Z)
+  >>> free x1 x2;
+  >>>
+  ```
+
+  ```
+  >>> [y1, y2, y3]~[Z, S(Z), S(S(Z))];
+  (4 interactions, 0.00 sec)
+  >>> y1 y2 y3;
+  Z S(Z) S(S(Z))
+  >>> free y1 y2 y3;
+  >>>
+  ```
+
+#### Append a list to the end of another list
+We also have a built-in agent `Append` to append a list `listB` to the end of another list `listA` as shown in the following pseudo code:
+
+```
+Append(r, listB) ~ listA --> r ~ (listA ++ listB)  // pseudo code
+```
+The order `listB` and `listA` seems something strange, so a special abbreviation notation is prepared:
+```
+r << Append(listA, listB)   == for ==  Append(r, listB)~listA
+```
+
+
+
+
+  ```
+  >>> Append(r, [Z, S(Z)]) ~ [A,B,C];
+  (4 interactions, 0.00 sec)
+  >>> r;
+  [A,B,C,Z,S(Z)]
+  >>> free r;
+  >>>
+  ```
+
+* The abbreviation notation for the Append:
+  ```
+  >>> r << Append([A,B,C], [Z, S(Z)]);
+  (4 interactions, 0.00 sec)
+  >>> r;
+  [A,B,C,Z,S(Z)]
+  >>> free r;
+  >>>
+  ```
+
+#### `Zip`: It makes two lists into a list of pairs
+A built-in agent `Zip` takes two lists and returns a list whose elements are pairs of the given two lists elements such that:
+```
+Zip(r,[A,B,...])~[AA,BB,...] -->* r~[(A,AA),(B,BB),...].
+```
+The length of the result will be the same to the shorter one in the given lists:
+```
+Zip(r,[A,B])~[AA,BB,CC,...] -->* r~[(A,AA),(B,BB)].
+```
+We can write it with the abbreviation as well:
+```
+>>> r << Zip([A,B,C], [AA,BB,CC]);
+(8 interactions, 0.00 sec)
+>>> r; free r;
+[(A,AA),(B,BB),(C,CC)]
+>>>
+```
+
+
+### Eraser
+
+* Eraser agent `Eraser` disposes any nets gradually:
+  ![Eraser](pic/eraser.png)
+  
+  ```
+  >>> Eraser ~ A(x1,x2);
+  (1 interactions, 0.00 sec)
+  >>> x1 x2;
+  Eraser Eraser
+  >>> free x1 x2;
+  >>>
+  ```
+
+
+### Duplicator
+* `Dup` agent duplicates any agents:
+  ![Dup](pic/dup.png)
+  ```
+  >>> Dup(a1,a2) ~ [Z, S(Z), S(S(Z))];
+  (10 interactions, 0.00 sec)
+  >>> a1 a2;
+  [Z,S(Z),S(S(Z))] [Z,S(Z),S(S(Z))]
+  >>> free a1 a2;
+  >>>
+  ```
+
+
+## Attributes (integers)
+
+Agents are extended so that integers can be held on their ports. These integers are called *attributes*. 
+
+* For instance, `A(100)` is an agent `A` that holds an attribute value `100`.
+
+  ```
+  >>> x~A(100);
+  (0 interactions, 0.01 sec)
+  >>> x;
+  A(100);
+  >>> free x;
+  >>>
+  ```
+
+
+### Built-in anonymous agent for attributes
+We can use integers the same as agents, and these are recognised as attributes of a built-in *anonymous agent* in Inpla. For instance, we can write `x~100` where the `100` is an attribute value of the anonymous agent. 
+
+
+  ```
+  >>> x~100;    // The `100' is regarded as an attribute of an anonymous agent
+  (0 interactions, 0.00 sec)
+  >>> x;
+  100
+  >>> free x;
+  >>>
+  ```
+
+
+
+### Arithmetic expressions on attributes
+It is possible to have attributes as calculation results of arithmetic operation using `where` statement after connections:  
+
+```
+<connections-with-expressions> ::= 
+                         <connections> 
+                       | <connections> 'where' <let-clause>* ';'
+                       
+<let-clause> ::= <name> '=' <arithmetic expression>
+```
+
+The symbol of addition, subtraction, multiplication, division, modulo are `+`, `-`, `*`, `/` and `%`, respectively. Relational operations `==`, `!=` `<`, `<=`, `>` and `>=` return 1 for True, 0 for False. Logical operations Not `!` (`not`), And `&&` (`and`)  and Or `||` (`or`) are also available where only `0` is regarded as False.
+
+* Example: an expression using `where`:
+
+  ```
+  >>> x~A(a) where a=3+5;
+  (0 interactions, 0.00 sec)
+  >>> x;
+  A(8)
+  >>> free x;
+  >>>
+  ```
+
+* Arithmetic expressions can be also written in arguments directly:
+
+  ```
+  >>> x~A(3+5);
+  (0 interactions, 0.00 sec)
+  >>> x;
+  A(8)
+  >>> free x;
+  >>>
+  ```
+
+
+* Arithmetic expressions are also available for the anonymous agent:
+
+  ```
+  >>> x~(3+5);  // this is also written without brackets as x~3+5;
+  (0 interactions, 0.00 sec)
+  >>> x;
+  8
+  >>> free x;
+  >>>
+  ```
+
+
+### Interaction rules with expressions on attributes
+In interaction rules, attributes are recognised by using variables with a modifier `int` in the rule-agent parts , and we call these *attribute variables*. 
+**Attribute variables has no Linear restriction** because these do not affect keeping the one-to-one connection among agent ports. So, we can use the same attribute variable as many times as we want.
+
+* Example: Incrementor on an attribute:
+
+  ```
+  >>> inc(result) >< (int a) => result~(a+1);  // The `a' is a variable for an attribute
+  >>> inc(r)~10;                               // This is also written as:  r << inc(10)
+  (1 interactions, 0.00 sec)
+  >>> r;
+  11
+  >>> free r;
+  >>>
+  ```
+
+
+- Example: Duplicator of integer lists. 
+
+  ![dup_list](pic/dup_list.png)
+  
+  
+  This has been implemented as a built-in agent `Dup`, but let's take it as an example that the same attribute variable occurs twice. On the first line of the following execution example, twice occurrences of *i*  in the right-hand side (here, `(i:xs1)` and `(i:xs2)`) is allowed in a rule. This is possible because the *i* is an attribute variable.
+
+  ```
+  >>> dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs;
+  >>> dup(a1,a2) >< []         => a1~[], a2~[];
+  >>> dup(a,b) ~ [1,2,3];    // This is also written as:   a,b << dup([1,2,3])
+  (2 interactions, 0.00 sec)
+  >>> a b;
+  [1,2,3] [1,2,3]
+  >>> free a b;
+  >>>
+  ```
+  
+  
+
+**We should be careful for operations of two attributes on distinct agents**. For instance, we take the following rule of an `add` agent, of course, it works as an addition operation on two attributes:
+
+```
+>>> add(result, int b) >< (int a) => result~(a+b);
+>>> add(r, 3) ~ 5;
+(1 interactions, 0.00 sec)
+>>> r;
+8
+>>> free r;
+>>>
+```
+
+However, it will cause a runtime error if the `add` rule is invoked without an attribute value on the second argument.  For instance, we take the following computation:
+
+```
+>>> b~1;
+>>> add(r, b)~3;
+>>> r;
+47005050212003
+>>>
+```
+
+This is because although it is not an attribute value, just a name, the `b` is recognised as an attribute value and the calculation is carried out.  To prevent this fragile situation, **we have to have extra rules to ensure that every port with the modifier `int` has been connected to an attribute**. For the rule of the `add`, the following is a **solution** to have the extra rule (the `addn` is introduced as the extra agent):
+
+```
+>>> add(result, b) >< (int a) => addn(result, a) ~ b;
+>>> addn(result, int a) >< (int b) => r~(a+b);
+```
+Do not worry about it. Some built-in rules for arithmetic computations are prepared as follows:
+
+
+### Built-in rules of attributes in the anonymous agents
+
+There are built-in rules for arithmetic operations between two agents by using `Add`, `Sub`, `Mul`, `Div`, `Mod` agents as addition, subtraction, multiplication, division and modulo, respectively. Rules for the `Add` are defined so that it can join two attributes on distinct agents safely as follows, and the others are also defined the same way:
+
+```
+Add(result, y)><(int x) => _Add(result, x)~y;
+_Add(result, int x)><(int y) => result~(x+y);
+```
+
+* Example:
+
+  ```
+  >>> Add(r,3)~5;    // Add is already defined as built-in.
+  >>> r;
+  8
+  >>> Sub(r1, r)~2;  // It is also written as an abbreviation form: r1<<Sub(r,2);
+  >>> r1;
+  6
+  >>>
+  ```
+
+  
+
+### Interaction rules with conditions on attributes
+Conditional rewritings on attributes are available. The following is a general form:  
+
+```
+<rule-with-conditions> ::= 
+  <agent> '><' <agent>
+  '|' <condition-on-attributes> '=>' <connections-with-expressions>
+  '|' <condition-on-attributes> '=>' <connections-with-expressions>
+      ...  
+  '|' '_'  '=>' <connections-with-expressions> ';'
+  
+<condition-on-attributes> is an expression on attributes specified in the two <agent>.
+```
+
+The sequence of `<condition-on-attributes>` must be finished with the otherwise case `_`.
+
+* Example: The following shows rules to obtain a list that contains only even numbers:
+
+  ```
+  // Rules
+  evenList(result) >< [] => r~[];
+  evenList(result) >< (int x):xs
+  | x%2==0 => result~(x:cnt), evenList(cnt)~xs
+  | _      => evenList(result)~xs;
+  ```
+
+  ```
+  >>> evenList(r)~[1,3,7,5,3,4,9,10];
+  >>> r;
+  [4,10]
+  >>> free r;
+  >>>
+  ```
+
+
+
+- Example: Fibonacci number:
+
+  ```
+  fib(r) >< (int n)
+  | n == 0 => r~0
+  | n == 1 => r~1
+  | _ => fib(r1)~(n-1), fib(r2)~(n-2), Add(r, r2)~r1;
+  
+  // * We cannot write result~(r1+r2) for Add(result, r2)~r1
+  // because r1, r2 may have not been connected to attributes in the anonymous agents,
+  // thus we have to leave the addition until both fib(r1)~(n-1), fib(r2)~(n-2) are finished.
+  // For this purpose we have to use the addition operation between agents defined as 
+  //   Add(result, y)><(int x) => _Add(result, x)~y;
+  //   _Add(result, int x)><(int y) => result~(x+y);
+  // By using Add(result, r2)~r1, 
+  // after r1,r2 have been connected to (int x), (int y), respectively, 
+  // x+y is executed and the calculation result is connected to the result safely.
+  ```
+  
+  ```
+  >>> fib(r)~39;
+  >>> r;
+  63245986
+  >>> free r;
+  >>>
+  ```
+  
+  
+
+## Commands
+
+Inpla has the following commands:
+* `free` *name1* ... *name_n* `;`     
+  The *name1* ... *name_n* and connected terms from these are disposed. To dispose all living names and connected terms, type `free ifce;`, where the `ifce` is an abbreviation of *interface* that is called for the set of names that live and occur once.
+  
+* *name1* ... *name_n* `;`  
+  Output terms connected from the *name1* ... *name_n*.
+  
+* `ifce;`
+
+  Output every term connected from the interface.
+
+* `prnat` *name*`;`    
+  Output a term connected from the *name* as a natural number.
+  
+* `memstat`;
+  
+  Output memory usage information for agent and name nodes. Only available in the single thread mode.
+  
+* `use` `"`*filename*`";`  
+  Read the file whose name is *filename*. 
+  
+* `exit;`            
+  Quit the system.
+
+Inpla has the following macro:
+* `const` *NAME*`=` *i* `;`  
+    The *NAME*  is bound to the integer value *i* as immutable, and replaced with the value *i* in nets and interaction rules.
+
+
+
+## Execution Options
+
+* When invoking Inpla, you can specify the following options:
+
+  ```
+  $ ./inpla -h
+  Inpla version 0.12.2
+  Usage: inpla [options]
+  
+  Options:
+   -f <filename>    Set input file name                     (Default:      STDIN)
+   -d <Name>=<val>  Bind <val> to <Name>
+   -Xms <num>       Set initial heap size to 2^<num>        (Defalut: 12 (=4096))
+   -Xmt <num>       Set multiple heap increment to 2^<num>  (Defalut:  3 (=   8))
+                      0: the same (=2^0) size heap is inserted when it runs up.
+                      1: the heap size is twice (=2^1).
+                      2: the size is four times (=2^2).
+   -Xes <num>       Set initial equation stack size         (Default:        256)
+   -w               Enable Weak Reduction strategy          (Default:    disable)
+   -c               Enable output of compiled codes         (Default:    disable)
+   -h               Print this help message
+   -foptimise-tail-calls  Enable tail call optimisation     (Default:    disable)
+  
+  Inpla version 0.12.0
+  Usage: inpla [options]
+  
+  Options:
+   -f <filename>    Set input file name                     (Default:      STDIN)
+   -d <Name>=<val>  Bind <val> to <Name>
+   -Xms <num>       Set initial heap size to 2^<num>        (Default: 12 (=4096))
+   -Xmt <num>       Set multiple heap increment to 2^<num>  (Default:  3 (=   8))
+                      0: the same size heap is inserted when it runs up.
+                      1: the twice (=2^1) size heap is inserted.
+   -Xes <num>       Set initial equation stack size         (Default:        256)
+   -t <num>         Set the number of threads               (Default:          8)
+   -w               Enable Weak Reduction strategy          (Default:      false)
+   -c               Enable to output compiled codes         (Default:    disable)
+   -h               Print this help message
+   -foptimise-tail-calls  Enable tail call optimisation     (Default:    disable)
+  ```
+
+**Note**: 
+
+* The option `-w` is available for the single-thread version.
+* The option ```-t``` is available for the multi-thread version that is compiled by ```make thread```. The default value is setting for the number of cores, so execution will be automatically scaled without specifying this. 
+* The option `-foptimise-tail-calls` enables the optimisation of tail calls. If the last equation in a rule has the reuse annotations, this optimisation is cancelled.
+
+
+## Advanced topics
+
+### Wildcard agent in rule definitions
+
+In rule definitions, we can place a variable as a default match on the left or right side of an active pair. For example, we suppose that we define the following rules:
+
+```
+reverse(r) >< [] => r~[];
+reverse(r) >< x:xs => rev_sub(r, [])~x:xs;
+
+rev_sub(r,ys) >< [] => r~ys;
+rev_sub(r,ys) >< x:xs => rev_sub(r,x:ys)~xs;
+```
+
+Using the wildcard agent notation, the `reverse` rule is simply written:
+
+```
+reverse(r) >< [] => r~[];
+reverse(r) >< xs => rev_sub(r, [])~xs;
+```
+
+The process of searching for rules of active pairs is as follows:
+
+- First, user-defined rules are searched for,
+- Next, built-in rules,
+- Finally, rules containing the wildcards,
+- Otherwise, runtime error.
+
+
+
+### Reuse annotations
+
+In interaction rule definitions, we can specify how active pair agents are reused by putting annotations `(*L)` and `(*R)` before agents in the right-hand side net. This annotations promote in-place computing, and as a result performance can be improved well  in parallel execution.
+
+* For instance, in the rule `gcd(ret) >< (int a, int b)`, we can reuse the `gcd` and `Tuple2` in nets as follows:
+
+  ```
+  gcd(ret) >< (int a, int b)
+  | b==0 => ret ~ a
+  | _ => (*L)gcd(ret) ~ (*R)(b, a%b);
+  ```
+
+
+
+### Built-in agents more
+
+* **Merger agent** `Merger`: 
+  it merges two lists into one. Merger agent has two principal ports that can take the two distinct lists. Interactions with the lists are performed as soon as one of the principal ports is connected one of the lists. So, the merged result is non-deterministically decided, especially in multi-threaded execution.
+  
+  ![merger](pic/merger.png)
+  
+  We overload `<<` in order to use the Merger agent naturally as follows:
+
+  ```
+  ret << Merger(alist, blist)
+  ```
+
+  The following is an execution example (the count of interactions is not supported yet):
+  ```
+  >>> r << Merger([0,0,0,0,0,0,0,0,0,0], [1,1,1,1,1,1,1,1,1,1]); 
+  (1 interactions by 4 threads, 0.10 sec)
+  >>> ifce;
+  r 
+  
+  Connections:
+  r ->[0,0,1,1,1,1,1,1,1,1,1,1,0,0,0,0,0,0,0,0]
+  
+  >>> 
+  ```
+
+
+
+### Map and reduce functions
+
+* **Lambda-application-like computation**: We can leave an interaction later by using a couple of Tuple2 agents. For instance, an destructor agent `foo` whose arity is 1 can be abstracted as `(r, foo(r))`, and we can give a constructor `s` later:
+  ```
+  (r, foo(r)) >< (result, s) -->* foo(result)~s.
+  
+  // where the following rule has been defined as a built-in:
+  // (a1,a2) ><> (b1,b2) => a1~b1, a2~b2.   
+  ```
+* **Map function operation**: So, the map function operation can be realised by a built-in `Map` agent with the following already defined rules:
+  ```
+  Map(result, f) >< []   => result~[], Eraser~f;
+  Map(result, f) >< x:xs => Dup(f1,f2)~f, 
+                            result~w:ws, 
+                            f1 ~ (w, x), Map(ws, f2)~xs;
+  ```
+  Actually, by using the incrementor `inc` we can add one to each list element:
+  ```
+  inc(r)><(int i) => r~(i+1);
+  Map( result, (r,inc(r)) ) ~ [10,20,30]
+   -->   Dup(f1,f2)~(r,inc(r)), result~w:ws, f1~(w,10), Map(ws,f2)~[20,30]
+   -->*  result~w:ws, (r1,inc(r1))~(w,10), Map( ws, (r2,inc(r2)) )~[20,30]
+   -->*  result~w:ws, inc(w)~10, Map( ws, (r2,inc(r2)) )~[20,30]
+   -->   result~w:ws, w~11, Map(ws, (r2,inc(r2)) )~[20,30]
+   -->   result~11:ws, Map(ws, (r2,inc(r2)) )~[20,30]
+   -->*  result~11:21:ws, Map(ws, (r3,inc(r3)) )~[30]
+   -->*  result~11:21:31:ws, Map(ws, (r4,inc(r4)) )~[]
+   -->*  result~[11,21,31];
+  ```
+  The Tuple2 agent seems a little complicated, so we prepare an abbreviation `%`. In the following, `foo1`, `foo2`, `foo3`, ... are any agents whose arity is 1, 2, 3, ..., respectively.
+  ```
+  The abbreviation form is decided according to the arity of a given agent to the %.
+  %foo1  === (r, foo1(r))
+  %foo2  === ((r,x), foo2(r,x))
+  %foo3  === ((r,x,y), foo3(r,x,y))
+  %foo4  === ((r,x,y,z), foo4(r,x,y,z))
+  %foo5  === ((r,x,y,z,zz), foo5(r,x,y,z,zz))
+    where r,x,y,z,zz are fresh names.
+  ```
+  For instance, by using %five we can write the following computation simply:
+  ```
+  %five ~ ((result,1,2,3,4), 5) -->* five(result,1,2,3,4)~5.
+  ```
+  This is quite useful for the map application. The `inc` application is written simply as follows:
+  ```
+  >>> Map(result, %inc) ~ [1,2,3];
+  >>> result;
+  [2,3,4]
+  >>>
+  ```
+  Wonderful!
+
+* **Reduce function operation**: The same as the map operation, we can define foldr and foldl as follows (Do not worry if it looks complicated. It is OK if we can just use these!):
+  ```
+  // --------------------------------------------------------------------
+  // foldr f v [x0, x1, ..., xn] = f(x0, f(x1, ... f(xn-1, f(xn, v))...))
+  // --------------------------------------------------------------------
+  foldr(r, f, v) >< x:xs => foldr_Cons(r,f,v,x)~xs;
+  foldr_Cons(r,f,v,x) >< [] => f~((r,x),v);
+  foldr_Cons(r,f,v,x) >< y:ys => 
+           Dup(f1,f2)~f,
+           foldr(w, f2, v)~y:ys,
+           f1~((r,x),w);
+  
+  // --------------------------------------------------------------------
+  // foldl f v [x0, x1, ..., xn] = f( ... f(f(v,x0),x1) ..., xn)
+  // --------------------------------------------------------------------
+  foldl(r, f, v) >< x:xs => foldl_Cons(r,f,v,x)~xs;    
+  foldl_Cons(r,f,v,x) >< [] => f~((r,v),x);
+  foldl_Cons(r,f,v,x) >< y:ys => 
+           Dup(f1,f2)~f,
+           f1~((w,v),x),
+           foldl(r, f2, w)~y:ys;
+  ```
+  These can be used quite simply:
+  ```
+  >>> foldr(r, %Sub, 1) ~ [30,20,10];  // 30-(20-(10-1)) = 30-(20-9) = 30-11 = 19
+  (17 interactions, 0.00 sec)
+  >>> r; free r;
+  19
+  >>> foldl(r, %Sub, 10) ~ [1,2,3]; //  ((10-1)-2)-3 = 4
+  (17 interactions, 0.00 sec)
+  >>> r; free r;
+  4
+  >>>
+  ```
+
+
+
+### Weak reduction strategy
+
+In this reduction strategy, only connections that have interface names (thus, live and occur once) are evaluated. This is taken for non-terminate computation such as fixed point combinator and process networks.
+
+* Example: We have a sample net in `sample/processnet1.in` that keep producing natural numbers from 1 and output these to the port `r`:
+
+  ```
+  // Rules
+  dup(a1,a2) >< (int i):xs => a1~(i:xs1), a2~(i:xs2), dup(xs1,xs2)~xs;
+  dup(a1,a2) >< []         => a1~[], a2~[];
+  
+  inc(r) >< (int i):xs => r~(i+1):w, inc(w)~xs;
+  inc(r) >< []         => r~[];
+  
+  // Nets
+  dup(r,w)~r1, inc(r1) ~ 0:w;
+  
+  //       +-----+       +-----+        +---+
+  // r ----|     |  r1   |     |        |   |
+  //       | dup |--->---| inc |---><---| 0 |----+
+  //   +---|     |       |     |        |   |    |
+  //   |   +-----+       +-----+        +---+    |
+  //   |                                         |
+  //   +-----------------------------------------+
+  //             w
+  ```
+
+  This reduction strategy is available by invoking with `-w` option as follows:
+
+  ```
+  $ ./inpla -w
+  Inpla 0.5.0 (Weak Strategy) : Interaction nets as a programming language [28 Oct. 2021]
+  >>> use "sample/processnet1.in";
+  (2 interactions, 0.00 sec)
+  >>> ifce;
+  r 
+  
+  Connections:
+  r ->[1,<a1>...    // this means a list of 1 and something.
+  
+  >>> a:b ~ r;
+  (2 interactions, 0.00 sec)
+  >>> ifce;
+  a b 
+  
+  Connections:
+  a ->1
+  b ->[2,<b1>...  
+  
+  >>>
+  ```
diff --git a/appunti b/appunti
deleted file mode 100644
index b64b282..0000000
--- a/appunti
+++ /dev/null
@@ -1,7 +0,0 @@
-scalability
-
-soundness of translated nn
-
-compatibility with other types of network
-
-comparison with other tool
diff --git a/nneq/__init__.py b/nneq/__init__.py
new file mode 100644
index 0000000..8dc7048
--- /dev/null
+++ b/nneq/__init__.py
@@ -0,0 +1,3 @@
+from .nneq import *
+
+__all__ = nneq.__all__
diff --git a/nneq/nneq.py b/nneq/nneq.py
new file mode 100644
index 0000000..22cf171
--- /dev/null
+++ b/nneq/nneq.py
@@ -0,0 +1,246 @@
+import z3
+import re
+import torch.fx as fx, torch.nn as nn
+import numpy as np
+import subprocess
+from typing import List, Dict
+
+__all__ = ["net", "strict_equivalence", "epsilon_equivalence", "argmax_equivalence"]
+
+type inpla_str = str
+type z3_str = str
+
+rules: inpla_str = """
+Linear(x, float q, float r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r);
+Concrete(float k) >< Add(out, b)
+	| k == 0 => out ~ b
+	| _ => b ~ AddCheckConcrete(out, k);
+Linear(y, float s, float t) >< AddCheckLinear(out, x, float q, float r)
+	| (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
+	| (s == 0) && (t == 0) => out ~ Linear(x, q, r), y ~ Eraser
+	| (q == 0) && (r == 0) => out ~ (*L)Linear(y, s, t), x ~ Eraser
+	| _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0);
+Concrete(float j) >< AddCheckLinear(out, x, float q, float r) => out ~ Linear(x, q, r + j);
+Linear(y, float s, float t) >< AddCheckConcrete(out, float k) => out ~ Linear(y, s, t + k);
+Concrete(float j) >< AddCheckConcrete(out, float k)
+	| j == 0 => out ~ Concrete(k)
+	| _ => out ~ Concrete(k + j);
+Linear(x, float q, float r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r);
+Concrete(float k) >< Mul(out, b)
+	| k == 0 => b ~ Eraser, out ~ (*L)Concrete(0)
+	| k == 1 => out ~ b
+	| _ => b ~ MulCheckConcrete(out, k);
+Linear(y, float s, float t) >< MulCheckLinear(out, x, float q, float r)
+	| ((q == 0) && (r == 0)) || ((s == 0) && (t == 0)) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
+	| _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0);
+Concrete(float j) >< MulCheckLinear(out, x, float q, float r) => out ~ Linear(x, q * j, r * j);
+Linear(y, float s, float t) >< MulCheckConcrete(out, float k) => out ~ Linear(y, s * k, t * k);
+Concrete(float j) >< MulCheckConcrete(out, float k)
+	| j == 0 => out ~ Concrete(0)
+	| j == 1 => out ~ Concrete(k)
+	| _ => out ~ Concrete(k * j);
+Linear(x, float q, float r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0);
+Concrete(float k) >< ReLU(out)
+	| k > 0 => out ~ (*L)Concrete(k)
+	| _ => out ~ Concrete(0);
+Linear(x, float q, float r) >< Materialize(out)
+	| (q == 0) => out ~ Concrete(r), x ~ Eraser
+	| (q == 1) && (r == 0) => out ~ x
+	| (q == 1) && (r != 0) => out ~ TermAdd(x, Concrete(r))
+	| (q != 0) && (r == 0) => out ~ TermMul(Concrete(q), x)
+	| _ => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r));
+Concrete(float k) >< Materialize(out) => out ~ (*L)Concrete(k);
+"""
+
+class NameGen:
+    def __init__(self):
+        self.counter = 0
+    def next(self) -> str:
+        name = f"v{self.counter}"
+        self.counter += 1
+        return name
+
+def inpla_export(model: nn.Module, input_shape: tuple) -> inpla_str:
+   traced = fx.symbolic_trace(model)
+   name_gen = NameGen()
+   script: List[str] = []
+   wire_map: Dict[str, List[str]] = {}
+   
+   for node in traced.graph.nodes:
+       if node.op == 'placeholder':
+           num_inputs = int(np.prod(input_shape))
+           wire_map[node.name] = [f"Linear(Symbolic(X_{i}), 1.0, 0.0)" for i in range(num_inputs)]
+
+       elif node.op == 'call_module':
+           target_str = str(node.target)
+           module = dict(model.named_modules())[target_str]
+           
+           input_node = node.args[0]
+           if not isinstance(input_node, fx.Node):
+               continue
+           input_wires = wire_map[input_node.name]
+
+           if isinstance(module, nn.Flatten):
+               wire_map[node.name] = input_wires
+
+           elif isinstance(module, nn.Linear):
+               W = (module.weight.data.detach().cpu().numpy()).astype(float)
+               B = (module.bias.data.detach().cpu().numpy()).astype(float)
+               out_dim, in_dim = W.shape
+               
+               neuron_wires = [f"Concrete({B[j]})" for j in range(out_dim)]
+
+               for i in range(in_dim):
+                   in_term = input_wires[i] 
+                   if out_dim == 1:
+                       weight = float(W[0, i])
+                       if weight == 0:
+                           script.append(f"Eraser ~ {in_term};")
+                       elif weight == 1:
+                           new_s = name_gen.next()
+                           script.append(f"Add({new_s}, {in_term}) ~ {neuron_wires[0]};")
+                           neuron_wires[0] = new_s
+                       else:
+                           mul_out = name_gen.next()
+                           new_s = name_gen.next()
+                           script.append(f"Mul({mul_out}, Concrete({weight})) ~ {in_term};")
+                           script.append(f"Add({new_s}, {mul_out}) ~ {neuron_wires[0]};")
+                           neuron_wires[0] = new_s
+                   else:
+                       branch_wires = [name_gen.next() for _ in range(out_dim)]
+                       
+                       def nest_dups(names: List[str]) -> str:
+                           if len(names) == 1: return names[0]
+                           if len(names) == 2: return f"Dup({names[0]}, {names[1]})"
+                           return f"Dup({names[0]}, {nest_dups(names[1:])})"
+                       
+                       script.append(f"{nest_dups(branch_wires)} ~ {in_term};")
+                       
+                       for j in range(out_dim):
+                           weight = float(W[j, i])
+                           if weight == 0:
+                               script.append(f"Eraser ~ {branch_wires[j]};")
+                           elif weight == 1:
+                               new_s = name_gen.next()
+                               script.append(f"Add({new_s}, {branch_wires[j]}) ~ {neuron_wires[j]};")
+                               neuron_wires[j] = new_s
+                           else:
+                               mul_out = name_gen.next()
+                               new_s = name_gen.next()
+                               script.append(f"Mul({mul_out}, Concrete({weight})) ~ {branch_wires[j]};")
+                               script.append(f"Add({new_s}, {mul_out}) ~ {neuron_wires[j]};")
+                               neuron_wires[j] = new_s
+
+               wire_map[node.name] = neuron_wires
+
+           elif isinstance(module, nn.ReLU):
+               output_wires = []
+               for i, w in enumerate(input_wires):
+                   r_out = name_gen.next()
+                   script.append(f"ReLU({r_out}) ~ {w};")
+                   output_wires.append(r_out)
+               wire_map[node.name] = output_wires
+
+       elif node.op == 'output':
+           output_node = node.args[0]
+           if isinstance(output_node, fx.Node):
+               final_wires = wire_map[output_node.name]
+               for i, w in enumerate(final_wires):
+                   res_name = f"result{i}"
+                   script.append(f"Materialize({res_name}) ~ {w};")
+                   script.append(f"{res_name};")
+
+   return "\n".join(script)
+
+def inpla_run(model: inpla_str) -> z3_str:
+    return subprocess.run(["./inpla"], input=f"{rules}\n{model}", capture_output=True, text=True).stdout
+
+syms = {}
+def Symbolic(id):
+    if id not in syms:
+        syms[id] = z3.Real(id)
+    return syms[id]
+
+def Concrete(val): return z3.RealVal(val)
+
+def TermAdd(a, b): return a + b
+def TermMul(a, b): return a * b
+def TermReLU(x): return z3.If(x > 0, x, 0)
+
+context = {
+   'Concrete': Concrete,
+   'Symbolic': Symbolic,
+   'TermAdd': TermAdd,
+   'TermMul': TermMul,
+   'TermReLU': TermReLU
+}
+
+wrap = re.compile(r"Symbolic\((.*?)\)")
+
+def z3_evaluate(model: z3_str):
+    model = wrap.sub(r'Symbolic("\1")', model);
+    return eval(model, context)
+
+def net(model: nn.Module, input_shape: tuple):
+    return z3_evaluate(inpla_run(inpla_export(model, input_shape)))
+
+
+def strict_equivalence(net_a, net_b):
+    solver = z3.Solver()
+
+    for sym in syms.values():
+        solver.add(z3.Or(sym == 0, sym == 1))
+
+    solver.add(net_a != net_b)
+
+    result = solver.check()
+
+    print("Strict Equivalence")
+    if result == z3.unsat:
+        print("VERIFIED: The networks are strictly equivalent.")
+    elif result == z3.sat:
+        print("FAILED: The networks are different.")
+        print("Counter-example input:")
+        print(solver.model())
+    else:
+        print("UNKNOWN: Solver could not decide.")
+
+def epsilon_equivalence(net_a, net_b, epsilon):
+    solver = z3.Solver()
+
+    for sym in syms.values():
+        solver.add(z3.Or(sym == 0, sym == 1))
+    
+    solver.add(z3.Abs(net_a - net_b) > epsilon)
+
+    result = solver.check()
+
+    print(f"Epsilon-Equivalence | Epsilon={epsilon}.")
+    if result == z3.unsat:
+        print("VERIFIED: The networks are epsilon-equivalent.")
+    elif result == z3.sat:
+        print("FAILED: The networks are different.")
+        print("Counter-example input:")
+        print(solver.model())
+    else:
+        print("UNKNOWN: Solver could not decide.")
+
+def argmax_equivalence(net_a, net_b):
+    solver = z3.Solver()
+
+    for sym in syms.values():
+        solver.add(z3.Or(sym == 0, sym == 1))
+    
+    solver.add((net_a > 0.5) != (net_b > 0.5))
+
+    result = solver.check()
+
+    print("ARGMAX Equivalence")
+    if result == z3.unsat:
+        print("VERIFIED: The networks are ARGMAX equivalent.")
+    elif result == z3.sat:
+        print("FAILED: The networks are different.")
+        print("Counter-example input:")
+        print(solver.model())
+    else:
+        print("UNKNOWN: Solver could not decide.")
diff --git a/notes.norg b/notes.norg
new file mode 100644
index 0000000..66dcbd9
--- /dev/null
+++ b/notes.norg
@@ -0,0 +1,93 @@
+@document.meta
+title: Neural Network Equivalence
+description: WIP tool to prove NNEQ using Interaction Nets as pre-processor
+authors: ericmarin
+categories: research
+created: 2026-03-14T09:21:24
+updated: 2026-03-14T18:34:04
+version: 1.1.1
+@end
+
+* TODO
+	- (?) Scalability %Maybe done? I have increased the limits of Inpla, but I have yet to test%
+	- ( ) Soundness of translated NN
+	~~ Define the semantic of the Agents (give a mathematical definition)
+	~~ Prove that a Layer L and the Inpla translation represent the same function
+	~~ Prove that each Interaction Rules preserve the mathematical semantic of the output
+	- ( ) Compatibility with other types of NN
+	- ( ) Comparison with other tool ({https://github.com/NeuralNetworkVerification/Marabou}[Marabou], {https://github.com/guykatzz/ReluplexCav2017}[Reluplex])
+	- ( ) Add Range agent to enable ReLU optimization
+
+* Agents
+** Built-in
+	 - Eraser: delete other agents recursively
+	 - Dup: duplicates other agents recursively
+
+** Implemented
+	 - Linear(x, float q, float r): represent "q*x + r"
+	 - Concrete(float k): represent a concrete value k
+	 - Symbolic(id): represent the variable id
+	 - Add(out, b): represent the addition (has various steps AddCheckLinear/AddCheckConcrete)
+	 - Mul(out, b): represent the multiplication (has various steps MulCheckLinear/MulCheckConcrete)
+	 - ReLU(out): represent "if x > 0 ? x ; 0"
+	 - Materialize(out): transforms a Linear packet into a final representation of TermAdd/TermMul
+
+* Rules
+** Add
+	 Linear(x, float q, float r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r);
+
+	 Concrete(float k) >< Add(out, b)
+	 | k == 0 => out ~ b
+	 | _ => b ~ AddCheckConcrete(out, k);
+
+	 Linear(y, float s, float t) >< AddCheckLinear(out, x, float q, float r)
+	 | (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
+	 | (s == 0) && (t == 0) => out ~ Linear(x, q, r), y ~ Eraser
+	 | (q == 0) && (r == 0) => out ~ (*L)Linear(y, s, t), x ~ Eraser
+	 | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0);
+
+	 Concrete(float j) >< AddCheckLinear(out, x, float q, float r) => out ~ Linear(x, q, r + j);
+
+	 Linear(y, float s, float t) >< AddCheckConcrete(out, float k) => out ~ Linear(y, s, t + k);
+
+	 Concrete(float j) >< AddCheckConcrete(out, float k)
+	 | j == 0 => out ~ Concrete(k)
+	 | _ => out ~ Concrete(k + j);
+
+** Mul
+	 Linear(x, float q, float r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r);
+
+	 Concrete(float k) >< Mul(out, b)
+	 | k == 0 => b ~ Eraser, out ~ (*L)Concrete(0)
+	 | k == 1 => out ~ b
+	 | _ => b ~ MulCheckConcrete(out, k);
+
+	 Linear(y, float s, float t) >< MulCheckLinear(out, x, float q, float r)
+	 | ((q == 0) && (r == 0)) || ((s == 0) && (t == 0)) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
+	 | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0);
+
+	 Concrete(float j) >< MulCheckLinear(out, x, float q, float r) => out ~ Linear(x, q * j, r * j);
+
+	 Linear(y, float s, float t) >< MulCheckConcrete(out, float k) => out ~ Linear(y, s * k, t * k);
+
+	 Concrete(float j) >< MulCheckConcrete(out, float k)
+	 | j == 0 => out ~ Concrete(0)
+	 | j == 1 => out ~ Concrete(k)
+	 | _ => out ~ Concrete(k * j);
+
+** ReLU
+	 Linear(x, float q, float r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0);
+
+	 Concrete(float k) >< ReLU(out)
+	 | k > 0 => out ~ (*L)Concrete(k)
+	 | _ => out ~ Concrete(0);
+
+** Materialize
+	 Linear(x, float q, float r) >< Materialize(out)
+	 | (q == 0) => out ~ Concrete(r), x ~ Eraser
+	 | (q == 1) && (r == 0) => out ~ x
+	 | (q == 1) && (r != 0) => out ~ TermAdd(x, Concrete(r))
+	 | (q != 0) && (r == 0) => out ~ TermMul(Concrete(q), x)
+	 | _ => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r));
+
+	 Concrete(float k) >< Materialize(out) => out ~ (*L)Concrete(k);
diff --git a/prover.py b/prover.py
deleted file mode 100644
index 614cdb6..0000000
--- a/prover.py
+++ /dev/null
@@ -1,108 +0,0 @@
-import z3
-import re
-import sys
-
-syms = {}
-def Symbolic(id):
-    if id not in syms:
-        syms[id] = z3.Real(id)
-    return syms[id]
-
-def Concrete(val): return z3.RealVal(val)
-
-def TermAdd(a, b): return a + b
-def TermMul(a, b): return a * b
-def TermReLU(x): return z3.If(x > 0, x, 0)
-
-context = {
-   'Concrete': Concrete,
-   'Symbolic': Symbolic,
-   'TermAdd': TermAdd,
-   'TermMul': TermMul,
-   'TermReLU': TermReLU
-}
-
-def equivalence(net_a, net_b):
-    solver = z3.Solver()
-
-    for sym in syms.values():
-        solver.add(z3.Or(sym == 0, sym == 1))
-
-    solver.add(net_a != net_b)
-
-    result = solver.check()
-
-    if result == z3.unsat:
-        print("VERIFIED: The networks are equivalent.")
-    elif result == z3.sat:
-        print("FAILED: The networks are different.")
-        print("Counter-example input:")
-        print(solver.model())
-    else:
-        print("UNKNOWN: Solver could not decide.")
-
-def epsilon_equivalence(net_a, net_b, epsilon):
-    solver = z3.Solver()
-
-    for sym in syms.values():
-        solver.add(z3.Or(sym == 0, sym == 1))
-    
-    solver.add(z3.Abs(net_a - net_b) > epsilon)
-
-    result = solver.check()
-
-    if result == z3.unsat:
-        print(f"VERIFIED: The networks are epsilon equivalent, with epsilon={epsilon}.")
-    elif result == z3.sat:
-        print("FAILED: The networks are different.")
-        print("Counter-example input:")
-        print(solver.model())
-    else:
-        print("UNKNOWN: Solver could not decide.")
-
-def argmax_equivalence(net_a, net_b):
-    solver = z3.Solver()
-
-    for sym in syms.values():
-        solver.add(z3.Or(sym == 0, sym == 1))
-    
-    solver.add((net_a > 0.5) != (net_b > 0.5))
-
-    result = solver.check()
-
-    if result == z3.unsat:
-        print("VERIFIED: The networks are argmax equivalent.")
-    elif result == z3.sat:
-        print("FAILED: The networks are classification-different.")
-        print("Counter-example input:")
-        print(solver.model())
-    else:
-        print("UNKNOWN: Solver could not decide.")
-
-if __name__ == "__main__":
-   lines = [line.strip() for line in sys.stdin if line.strip() and not line.startswith("(")]
-   
-   if len(lines) < 2:
-       print(f"; Error: Expected at least 2 Inpla output strings, but got {len(lines)}.")
-       sys.exit(1)
-
-   try:
-       wrap = re.compile(r"Symbolic\((.*?)\)")
-       net_a_str = wrap.sub(r'Symbolic("\1")', lines[-2]);
-       net_b_str = wrap.sub(r'Symbolic("\1")', lines[-1]);
-       
-       print(f"Comparing:\nA: {net_a_str}\n\nB: {net_b_str}")
-       
-       net_a = eval(net_a_str, context)
-       net_b = eval(net_b_str, context)
-       
-       print("\nStrict Equivalence")
-       equivalence(net_a, net_b)
-       print("\nEpsilon-Equivalence")
-       epsilon_equivalence(net_a, net_b, 1e-1)
-       print("\nARGMAX Equivalence")
-       argmax_equivalence(net_a, net_b)
-
-   except Exception as e:
-       print(f"; Error parsing Inpla output: {e}")
-       sys.exit(1)
diff --git a/rules.in b/rules.in
deleted file mode 100644
index 22698bd..0000000
--- a/rules.in
+++ /dev/null
@@ -1,71 +0,0 @@
-// Agents
-// Built-in
-// Eraser: delete other agents recursively
-// Dup: duplicates other agents recursively
-
-// Implemented
-// Linear(x, float q, float r): represent "q*x + r"
-// Concrete(float k): represent a concrete value k
-// Symbolic(id): represent the variable id
-// Add(out, b): represent the addition (has various steps AddCheckLinear/AddCheckConcrete)
-// Mul(out, b): represent the multiplication (has various steps MulCheckLinear/MulCheckConcrete)
-// ReLU(out): represent "if x > 0 ? x ; 0"
-// Materialize(out): transforms a Linear packet into a final representation of TermAdd/TermMul/TermReLU
-
-// TODO: add range information to enable ReLU elimination
-
-// Rules
-Linear(x, float q, float r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r);
-
-Concrete(float k) >< Add(out, b)
-	| k == 0 => out ~ b
-	| _ => b ~ AddCheckConcrete(out, k);
-
-Linear(y, float s, float t) >< AddCheckLinear(out, x, float q, float r)
-	| (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
-	| (s == 0) && (t == 0) => Linear(x, q, r) ~ Materialize(out), y ~ Eraser
-	| (q == 0) && (r == 0) => (*L)Linear(y, s, t) ~ Materialize(out), x ~ Eraser
-	| _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0);
-
-Concrete(float j) >< AddCheckLinear(out, x, float q, float r) => out ~ Linear(x, q, r + j);
-
-Linear(y, float s, float t) >< AddCheckConcrete(out, float k) => out ~ Linear(y, s, t + k);
-
-Concrete(float j) >< AddCheckConcrete(out, float k)
-	| j == 0 => out ~ Concrete(k)
-	| _ => out ~ Concrete(k + j);
-
-Linear(x, float q, float r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r);
-
-Concrete(float k) >< Mul(out, b)
-	| k == 0 => b ~ Eraser, out ~ (*L)Concrete(0)
-	| k == 1 => out ~ b
-	| _ => b ~ MulCheckConcrete(out, k);
-
-Linear(y, float s, float t) >< MulCheckLinear(out, x, float q, float r)
-	| (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
-	| (s == 0) && (t == 0) => Linear(x, q, r) ~ Materialize(out), y ~ Eraser
-	| (q == 0) && (r == 0) => (*L)Linear(y, s, t) ~ Materialize(out), x ~ Eraser
-	| _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0);
-
-Concrete(float j) >< MulCheckLinear(out, x, float q, float r) => out ~ Linear(x, q * j, r * j);
-
-Linear(y, float s, float t) >< MulCheckConcrete(out, float k) => out ~ Linear(y, s * k, t * k);
-
-Concrete(float j) >< MulCheckConcrete(out, float k)
-	| j == 0 => out ~ Concrete(0)
-	| j == 1 => out ~ Concrete(k)
-	| _ => out ~ Concrete(k * j);
-
-Linear(x, float q, float r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0);
-
-Concrete(float k) >< ReLU(out)
-	| k > 0 => out ~ (*L)Concrete(k)
-	| _ => out ~ Concrete(0);
-
-Linear(x, float q, float r) >< Materialize(out)
-	| (q == 0) => out ~ Concrete(r), x ~ Eraser
-	| (q == 1) && (r == 0) => out ~ x
-	| (q == 1) && (r != 0) => out ~ TermAdd(x, Concrete(r))
-	| (q != 0) && (r == 0) => out ~ TermMul(Concrete(q), x)
-	| _ => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r));
diff --git a/xor.in b/xor.in
deleted file mode 100644
index 6a71e7b..0000000
--- a/xor.in
+++ /dev/null
@@ -1,142 +0,0 @@
-// Agents
-// Built-in
-// Eraser: delete other agents recursively
-// Dup: duplicates other agents recursively
-
-// Implemented
-// Linear(x, float q, float r): represent "q*x + r"
-// Concrete(float k): represent a concrete value k
-// Symbolic(id): represent the variable id
-// Add(out, b): represent the addition (has various steps AddCheckLinear/AddCheckConcrete)
-// Mul(out, b): represent the multiplication (has various steps MulCheckLinear/MulCheckConcrete)
-// ReLU(out): represent "if x > 0 ? x ; 0"
-// Materialize(out): transforms a Linear packet into a final representation of TermAdd/TermMul/TermReLU
-
-// TODO: add range information to enable ReLU elimination
-
-// Rules
-Linear(x, float q, float r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r);
-
-Concrete(float k) >< Add(out, b)
-	| k == 0 => out ~ b
-	| _ => b ~ AddCheckConcrete(out, k);
-
-Linear(y, float s, float t) >< AddCheckLinear(out, x, float q, float r)
-	| (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
-	| (s == 0) && (t == 0) => Linear(x, q, r) ~ Materialize(out), y ~ Eraser
-	| (q == 0) && (r == 0) => (*L)Linear(y, s, t) ~ Materialize(out), x ~ Eraser
-	| _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0);
-
-Concrete(float j) >< AddCheckLinear(out, x, float q, float r) => out ~ Linear(x, q, r + j);
-
-Linear(y, float s, float t) >< AddCheckConcrete(out, float k) => out ~ Linear(y, s, t + k);
-
-Concrete(float j) >< AddCheckConcrete(out, float k)
-	| j == 0 => out ~ Concrete(k)
-	| _ => out ~ Concrete(k + j);
-
-Linear(x, float q, float r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r);
-
-Concrete(float k) >< Mul(out, b)
-	| k == 0 => b ~ Eraser, out ~ (*L)Concrete(0)
-	| k == 1 => out ~ b
-	| _ => b ~ MulCheckConcrete(out, k);
-
-Linear(y, float s, float t) >< MulCheckLinear(out, x, float q, float r)
-	| (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser
-	| (s == 0) && (t == 0) => Linear(x, q, r) ~ Materialize(out), y ~ Eraser
-	| (q == 0) && (r == 0) => (*L)Linear(y, s, t) ~ Materialize(out), x ~ Eraser
-	| _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0);
-
-Concrete(float j) >< MulCheckLinear(out, x, float q, float r) => out ~ Linear(x, q * j, r * j);
-
-Linear(y, float s, float t) >< MulCheckConcrete(out, float k) => out ~ Linear(y, s * k, t * k);
-
-Concrete(float j) >< MulCheckConcrete(out, float k)
-	| j == 0 => out ~ Concrete(0)
-	| j == 1 => out ~ Concrete(k)
-	| _ => out ~ Concrete(k * j);
-
-Linear(x, float q, float r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0);
-
-Concrete(float k) >< ReLU(out)
-	| k > 0 => out ~ (*L)Concrete(k)
-	| _ => out ~ Concrete(0);
-
-Linear(x, float q, float r) >< Materialize(out)
-	| (q == 0) => out ~ Concrete(r), x ~ Eraser
-	| (q == 1) && (r == 0) => out ~ x
-	| (q == 1) && (r != 0) => out ~ TermAdd(x, Concrete(r))
-	| (q != 0) && (r == 0) => out ~ TermMul(Concrete(q), x)
-	| _ => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r));
-
-
-// Network A
-Dup(v0, Dup(v1, Dup(v2, v3))) ~ Linear(Symbolic(X_0), 1.0, 0.0);
-Mul(v4, Concrete(1.249051570892334)) ~ v0;
-Add(v5, v4) ~ Concrete(-2.076689270325005e-05);
-Mul(v6, Concrete(0.8312496542930603)) ~ v1;
-Add(v7, v6) ~ Concrete(-0.8312351703643799);
-Mul(v8, Concrete(0.9251033663749695)) ~ v2;
-Add(v9, v8) ~ Concrete(-0.9250767230987549);
-Mul(v10, Concrete(0.3333963453769684)) ~ v3;
-Add(v11, v10) ~ Concrete(0.05585573986172676);
-Dup(v12, Dup(v13, Dup(v14, v15))) ~ Linear(Symbolic(X_1), 1.0, 0.0);
-Mul(v16, Concrete(0.8467237949371338)) ~ v12;
-Add(v17, v16) ~ v5;
-Mul(v18, Concrete(0.8312491774559021)) ~ v13;
-Add(v19, v18) ~ v7;
-Mul(v20, Concrete(0.9251176118850708)) ~ v14;
-Add(v21, v20) ~ v9;
-Mul(v22, Concrete(1.084873080253601)) ~ v15;
-Add(v23, v22) ~ v11;
-ReLU(v24) ~ v17;
-ReLU(v25) ~ v19;
-ReLU(v26) ~ v21;
-ReLU(v27) ~ v23;
-Mul(v28, Concrete(0.7005411982536316)) ~ v24;
-Add(v29, v28) ~ Concrete(-0.02095046266913414);
-Mul(v30, Concrete(-0.9663007259368896)) ~ v25;
-Add(v31, v30) ~ v29;
-Mul(v32, Concrete(-1.293721079826355)) ~ v26;
-Add(v33, v32) ~ v31;
-Mul(v34, Concrete(0.3750816583633423)) ~ v27;
-Add(v35, v34) ~ v33;
-Materialize(result0) ~ v35;
-result0;
-free ifce;
-
-
-// Network B
-Dup(v0, Dup(v1, Dup(v2, v3))) ~ Linear(Symbolic(X_0), 1.0, 0.0);
-Mul(v4, Concrete(1.1727254390716553)) ~ v0;
-Add(v5, v4) ~ Concrete(-0.005158121697604656);
-Mul(v6, Concrete(1.1684346199035645)) ~ v1;
-Add(v7, v6) ~ Concrete(-1.1664382219314575);
-Mul(v8, Concrete(-0.2502972185611725)) ~ v2;
-Add(v9, v8) ~ Concrete(-0.10056735575199127);
-Mul(v10, Concrete(-0.6796815395355225)) ~ v3;
-Add(v11, v10) ~ Concrete(-0.32640340924263);
-Dup(v12, Dup(v13, Dup(v14, v15))) ~ Linear(Symbolic(X_1), 1.0, 0.0);
-Mul(v16, Concrete(1.1758666038513184)) ~ v12;
-Add(v17, v16) ~ v5;
-Mul(v18, Concrete(1.1700055599212646)) ~ v13;
-Add(v19, v18) ~ v7;
-Mul(v20, Concrete(0.02409248612821102)) ~ v14;
-Add(v21, v20) ~ v9;
-Mul(v22, Concrete(-0.43328654766082764)) ~ v15;
-Add(v23, v22) ~ v11;
-ReLU(v24) ~ v17;
-ReLU(v25) ~ v19;
-ReLU(v26) ~ v21;
-ReLU(v27) ~ v23;
-Mul(v28, Concrete(0.8594199419021606)) ~ v24;
-Add(v29, v28) ~ Concrete(7.867255291671427e-09);
-Mul(v30, Concrete(-1.7184218168258667)) ~ v25;
-Add(v31, v30) ~ v29;
-Mul(v32, Concrete(-0.207244873046875)) ~ v26;
-Add(v33, v32) ~ v31;
-Mul(v34, Concrete(-0.14912307262420654)) ~ v27;
-Add(v35, v34) ~ v33;
-Materialize(result0) ~ v35;
-result0;
\ No newline at end of file
diff --git a/xor.py b/xor.py
index 493eaef..9ab7be7 100644
--- a/xor.py
+++ b/xor.py
@@ -1,11 +1,8 @@
 import torch
 import torch.nn as nn
-import torch.fx as fx
-import numpy as np
-import os
-from typing import List, Dict
+import nneq
 
-class XOR_MLP(nn.Module):
+class xor_mlp(nn.Module):
     def __init__(self, hidden_dim=4):
         super().__init__()
         self.layers = nn.Sequential(
@@ -16,124 +13,11 @@ class XOR_MLP(nn.Module):
     def forward(self, x):
         return self.layers(x)
 
-class NameGen:
-    def __init__(self):
-        self.counter = 0
-    def next(self) -> str:
-        name = f"v{self.counter}"
-        self.counter += 1
-        return name
-
-def get_rules() -> str:
-    rules_path = os.path.join(os.path.dirname(__file__), "rules.in")
-    if not os.path.exists(rules_path):
-        return "// Rules not found in rules.in\n"
-    
-    rules_lines = []
-    with open(rules_path, "r") as f:
-        for line in f:
-            if "// Net testing" in line:
-                break
-            rules_lines.append(line)
-    return "".join(rules_lines)
-
-def export_to_inpla_wiring(model: nn.Module, input_shape: tuple) -> str:
-   traced = fx.symbolic_trace(model)
-   name_gen = NameGen()
-   script: List[str] = []
-   wire_map: Dict[str, List[str]] = {}
-   
-   for node in traced.graph.nodes:
-       if node.op == 'placeholder':
-           num_inputs = int(np.prod(input_shape))
-           wire_map[node.name] = [f"Linear(Symbolic(X_{i}), 1.0, 0.0)" for i in range(num_inputs)]
-
-       elif node.op == 'call_module':
-           target_str = str(node.target)
-           module = dict(model.named_modules())[target_str]
-           
-           input_node = node.args[0]
-           if not isinstance(input_node, fx.Node):
-               continue
-           input_wires = wire_map[input_node.name]
-
-           if isinstance(module, nn.Flatten):
-               wire_map[node.name] = input_wires
-
-           elif isinstance(module, nn.Linear):
-               W = (module.weight.data.detach().cpu().numpy()).astype(float)
-               B = (module.bias.data.detach().cpu().numpy()).astype(float)
-               out_dim, in_dim = W.shape
-               
-               neuron_wires = [f"Concrete({B[j]})" for j in range(out_dim)]
-
-               for i in range(in_dim):
-                   in_term = input_wires[i] 
-                   if out_dim == 1:
-                       weight = float(W[0, i])
-                       if weight == 0:
-                           script.append(f"Eraser ~ {in_term};")
-                       elif weight == 1:
-                           new_s = name_gen.next()
-                           script.append(f"Add({new_s}, {in_term}) ~ {neuron_wires[0]};")
-                           neuron_wires[0] = new_s
-                       else:
-                           mul_out = name_gen.next()
-                           new_s = name_gen.next()
-                           script.append(f"Mul({mul_out}, Concrete({weight})) ~ {in_term};")
-                           script.append(f"Add({new_s}, {mul_out}) ~ {neuron_wires[0]};")
-                           neuron_wires[0] = new_s
-                   else:
-                       branch_wires = [name_gen.next() for _ in range(out_dim)]
-                       
-                       def nest_dups(names: List[str]) -> str:
-                           if len(names) == 1: return names[0]
-                           if len(names) == 2: return f"Dup({names[0]}, {names[1]})"
-                           return f"Dup({names[0]}, {nest_dups(names[1:])})"
-                       
-                       script.append(f"{nest_dups(branch_wires)} ~ {in_term};")
-                       
-                       for j in range(out_dim):
-                           weight = float(W[j, i])
-                           if weight == 0:
-                               script.append(f"Eraser ~ {branch_wires[j]};")
-                           elif weight == 1:
-                               new_s = name_gen.next()
-                               script.append(f"Add({new_s}, {branch_wires[j]}) ~ {neuron_wires[j]};")
-                               neuron_wires[j] = new_s
-                           else:
-                               mul_out = name_gen.next()
-                               new_s = name_gen.next()
-                               script.append(f"Mul({mul_out}, Concrete({weight})) ~ {branch_wires[j]};")
-                               script.append(f"Add({new_s}, {mul_out}) ~ {neuron_wires[j]};")
-                               neuron_wires[j] = new_s
-
-               wire_map[node.name] = neuron_wires
-
-           elif isinstance(module, nn.ReLU):
-               output_wires = []
-               for i, w in enumerate(input_wires):
-                   r_out = name_gen.next()
-                   script.append(f"ReLU({r_out}) ~ {w};")
-                   output_wires.append(r_out)
-               wire_map[node.name] = output_wires
-
-       elif node.op == 'output':
-           output_node = node.args[0]
-           if isinstance(output_node, fx.Node):
-               final_wires = wire_map[output_node.name]
-               for i, w in enumerate(final_wires):
-                   res_name = f"result{i}"
-                   script.append(f"Materialize({res_name}) ~ {w};")
-                   script.append(f"{res_name};")
-
-   return "\n".join(script)
-
 def train_model(name: str):
     X = torch.tensor([[0,0], [0,1], [1,0], [1,1]], dtype=torch.float32)
     Y = torch.tensor([[0], [1], [1], [0]], dtype=torch.float32)
 
-    net = XOR_MLP()
+    net = xor_mlp()
     loss_fn = nn.MSELoss()
     optimizer = torch.optim.Adam(net.parameters(), lr=0.01)
 
@@ -149,22 +33,16 @@ def train_model(name: str):
     return net
 
 if __name__ == "__main__":
-    # Train two different models
     net_a = train_model("Network A")
     net_b = train_model("Network B")
 
-    print("\nExporting both to xor.in...")
+    z3_net_a = nneq.net(net_a, (2,))
+    z3_net_b = nneq.net(net_b, (2,))
     
-    rules = get_rules()
-    wiring_a = export_to_inpla_wiring(net_a, (2,))
-    wiring_b = export_to_inpla_wiring(net_b, (2,))
+    print("")
+    nneq.strict_equivalence(z3_net_a, z3_net_b)
+    print("")
+    nneq.epsilon_equivalence(z3_net_a, z3_net_b, 0.1)
+    print("")
+    nneq.argmax_equivalence(z3_net_a, z3_net_b)
 
-    with open("xor.in", "w") as f:
-        f.write(rules)
-        f.write("\n\n// Network A\n")
-        f.write(wiring_a)
-        f.write("\nfree ifce;\n")
-        f.write("\n\n// Network B\n")
-        f.write(wiring_b)
-    
-    print("Done. Now run: inpla -f xor.in | python3 prover.py")