[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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:


    \A f,g \in bv4 : \A i \in 0..3 : AND4[f,g][i] <=> f[i] /\ g[i]


    <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.