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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Thu, 10 Nov 2022 10:06:35 +0100*References*: <a54e1db7-6807-4de1-bfdf-d7fe738a5ba8n@googlegroups.com>

Before diving into subproofs, it is good practice to get the overall structure of the proof right: start by checking if you can prove the level-1 QED step from the preceding level-1 steps. In your case, since you are claiming an equivalence, you'll need both your step <1>3 and the reverse implication. Your step <1>4 should be one of several level-2 steps beneath step <1>3. Below is how I would set up the proof, for bit vectors of arbitrary (but fixed) length. Note that the assumption that N is a natural number is not needed for this proof but will probably be useful elsewhere. Stephan ––– CONSTANT N
-- ASSUME NNat == N \in Nat BVN == [1 .. N -> BOOLEAN] bv_and(bv1, bv2) == [i \in 1 .. N |-> bv1[i] /\ bv2[i]] THEOREM ASSUME NEW bv1 \in BVN, NEW bv2 \in BVN, NEW i \in 1 .. N PROVE bv_and(bv1, bv2)[i] <=> bv1[i] /\ bv2[i] BY DEF BVN, bv_and
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/C80DC618-2D06-4746-8C89-4951E2A78E92%40gmail.com. |

**Follow-Ups**:

**References**:**[tlaplus] How can I prove AND function on 4 bit value in TLAPS***From:*Amjad Ali

- Prev by Date:
**[tlaplus] How can I prove AND function on 4 bit value in TLAPS** - Next by Date:
**Re: [tlaplus] How to add an auxiliary variable but not increase the state space?** - Previous by thread:
**[tlaplus] How can I prove AND function on 4 bit value in TLAPS** - Next by thread:
**Re: [tlaplus] How can I prove AND function on 4 bit value in TLAPS** - Index(es):