bv4 == [ 0..3 -> {TRUE,FALSE} ]
and a function that does an AND operation on two 4 bit values:
AND4 == [f,g \in bv4 |-> [i \in 0..3 |-> (i=0 /\ f[0] /\ g[0]) \/
(i=1 /\ f[1] /\ g[1]) \/
(i=2 /\ f[2] /\ g[2]) \/
(i=3 /\ f[3] /\ g[3]) ]]
This function should behave like any an AND operation in any assembly language. For example, AND 0b1010, 0b0010 == 0b0010
In TLA+, a 4-bit binary number is represented in a form of a function. So, AND4 takes in. two functions and outputs a function.
It's pretty straight forward to see that AND4 would behave as it should, but how can I prove it for any given 4-bit. values.
I tried starting it. Please tell me if I'm on the right track:
THEOREM AND4_CORRECT==
\A f,g \in bv4 : \A i \in 0..3 : AND4[f,g][i] <=> f[i] /\ g[i]
PROOF
<1>1 TAKE f,g \in bv4
<1>2 TAKE i \in 0..3
<1>3 ASSUME AND4[f,g][i] PROVE f[i] /\ g[i]
<1>4 CASE i = 0
<2>1 f[0] /\ g[0]
<2> QED
<1> QED
--
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/a54e1db7-6807-4de1-bfdf-d7fe738a5ba8n%40googlegroups.com.
BVN == [0..N -> {TRUE, FALSE}]
ANDN == [f,g \in BVN |-> [i \in 0..N |-> f[i] /\ g[i]]]
ANDN2(f,g) == [i \in 0..N |-> f[i] /\ g[i]]
THEOREM ANDN2_CORRECT==
\A f,g \in BVN : \A i \in 0..N :
ANDN2(f,g)[i] <=> f[i] /\ g[i]
PROOF
<1>1 TAKE f,g \in BVN
<1>2 TAKE i \in 0..N
<1>3 ANDN2(f,g)[i] <=> f[i] /\ g[i]
BY DEF BVN, ANDN2
<1> QED BY <1>3
THEOREM ANDN_CORRECT==
\A f,g \in BVN : \A i \in 0..N :
ANDN[f,g][i] <=> f[i] /\ g[i]
PROOF
<1>1 TAKE f,g \in BVN
<1>2 TAKE i \in 0..N
<1>3 ANDN[f,g][i] <=> f[i] /\ g[i] >>>>>>>>>>>>>>>>>>>> Fails Here
BY DEF BVN, ANDN
<1> QED BY <1>3
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4e50b05c-19bb-4673-ba06-7933b41412cen%40googlegroups.com.