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

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.