[tlaplus] How to simplify my CMP32 function in terms of N?

[Amjad Ali <amjad.hamdi.ali@xxxxxxxxx>]

Given the following  definitions below, how can I generalize my CMP32 function to work for any domain 0..N (like the XORN function)? The CMP function should have a range {TRUE, FALSE}. Which is TRUE when both inputs are equal and FALSE otherwise:

CONSTANT N

ASSUME NNAT == N \in Nat

BVN == [0..N -> {TRUE,FALSE}]

XORN == [f \in BVN |-> [g \in BVN |-> [i \in 0..N |-> ((f[i] /\ ~g[i]) \/ (~f[i] /\ g[i]))]]]

CMP32 == [f \in BVN |-> [g \in BVN |->  

                                       ~XORN[f][g][0]  /\ ~XORN[f][g][1]  /\ ~XORN[f][g][2]  /\ 

                                       ~XORN[f][g][3]  /\ ~XORN[f][g][4]  /\ ~XORN[f][g][5]  /\ 

                                       ~XORN[f][g][6]  /\ ~XORN[f][g][7]  /\ ~XORN[f][g][8]  /\

                                       ~XORN[f][g][9]  /\ ~XORN[f][g][10] /\ ~XORN[f][g][11] /\

                                       ~XORN[f][g][12] /\ ~XORN[f][g][13] /\ ~XORN[f][g][14] /\

                                       ~XORN[f][g][15] /\ ~XORN[f][g][16] /\ ~XORN[f][g][17] /\

                                       ~XORN[f][g][18] /\ ~XORN[f][g][19] /\ ~XORN[f][g][20] /\

                                       ~XORN[f][g][21] /\ ~XORN[f][g][22] /\ ~XORN[f][g][23] /\

                                       ~XORN[f][g][24] /\ ~XORN[f][g][25] /\ ~XORN[f][g][26] /\

                                       ~XORN[f][g][27] /\ ~XORN[f][g][28] /\ ~XORN[f][g][29] /\

                                       ~XORN[f][g][30] /\ ~XORN[f][g][31] ]]

I would like something like :

CMP32 == [f \in BVN |-> [g \in BVN |->  

                                       ~XORN[f][g][0]  /\ ~XORN[f][g][1]  /\ .. /\ ~XORN[f][g][N] 

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/823518f4-8176-47ed-9b68-9d8d6f7291f9n%40googlegroups.com.