From 2ee29a81ad49a82f02d03ac0ce7b2152299ee53f Mon Sep 17 00:00:00 2001 From: "Larry D. Lee Jr" Date: Fri, 11 Jan 2019 11:58:08 -0500 Subject: [PATCH] Proved the idempotent propert for wor. --- theories/Word.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/theories/Word.v b/theories/Word.v index 512e35e..de8bc95 100644 --- a/theories/Word.v +++ b/theories/Word.v @@ -1720,6 +1720,19 @@ Proof. unfold wor; induction sz; shatterer. Qed. +Lemma wor_idemp + : forall (n : nat) (x0 : word n), x0 ^| x0 = x0. +Proof. + (intros). + (induction x0). + reflexivity. + (rewrite <- IHx0 at 3). + (unfold wor). + (simpl). + (rewrite orb_diag). + reflexivity. +Qed. + Lemma wand_wones : forall sz w, wones sz ^& w = w. Proof. unfold wand; induction sz; shatterer.