# [tlaplus] How can I prove AND function on 4 bit value in TLAPS

I've defined a 4 bit value as such:

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a54e1db7-6807-4de1-bfdf-d7fe738a5ba8n%40googlegroups.com.