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