On 6 Nov 2022, at 06:57, Amjad Ali <amjad.h...@gmail.com> wrote:
I want to prove cmp_bv4 for all 4-bit binary numbers is correct. As seen below, a binary value of 4 bits is represented as a set of functions with domain 0-3 and range 0 and 1. Then, an xor function with domain 0 and 1 that outputs 0 if the two inputs match (or 1 other, otherwise). Finally, cmp_bv4 takes in two 4-bit binary numbers and uses the xor function to determine if the values match. Why do this and not just use (=) ? In the machine I'm building, a comparator is not available and I need to build one from scratch.
<Screen Shot 2022-11-06 at 12.43.42 AM.png>
--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bcd0ac97-be4f-4b5e-b91b-d347dde2cb61n%40googlegroups.com.
THEOREM NOT_XOR_EQ ==
\A x,y \in {TRUE, FALSE} : ~xor[x,y] => x=y
PROOF
<1> TAKE x,y \in {TRUE, FALSE}
<1>1 CASE x=FALSE /\ y=FALSE
<2>1 ~xor[x,y] = TRUE BY DEF xor
<2>2 QED BY <2>1
<1>2 x=FALSE /\ y=TRUE
<2>3 ~xor[x,y] = FALSE BY DEF xor
<2>4 QED BY <2>3
<1>3 x=TRUE /\ y=FALSE
<2>5 ~xor[x,y] = FALSE BY DEF xor
<2>6 QED BY <2>5
<1>4 x=TRUE /\ y=TRUE
<2>7 ~xor[x,y] = TRUE BY DEF xor
<2>8 QED BY <2>7
<1>5 QED BY <1>1, <1>2, <1>3, <1>4
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e9e17f38-0154-4a92-a34d-1559f0f78168n%40googlegroups.com.