#x; nelim x; #w1; #w2;
#y; nelim y; #w3; #w4;
nnormalize;
- napply (or_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_w32_aux1 w1 w2 w3 w4 H))
- ##| ##1: #H; napply (or_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
- ##[ ##2: #H1; napply (or_intror … (decidable_w32_aux2 w1 w2 w3 w4 H1))
+ napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w32_aux1 w1 w2 w3 w4 H))
+ ##| ##1: #H; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_w32_aux2 w1 w2 w3 w4 H1))
##| ##1: #H1; nrewrite > H; nrewrite > H1;
- napply (or_introl … (refl_eq ? 〈w3.w4〉))
+ napply (or2_intro1 … (refl_eq ? 〈w3.w4〉))
##]
##]
nqed.
#w1; #w2; #w3; #w4;
nchange with ((((eq_w16 w3 w1) ⊗ (eq_w16 w4 w2)) = false) → ?);
#H;
- napply (or_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false … H) …);
##[ ##1: #H1; napply (decidable_w32_aux1 … (neqw16_to_neq … H1))
##| ##2: #H1; napply (decidable_w32_aux2 … (neqw16_to_neq … H1))
##]
nlemma word32_destruct : ∀w1,w2,w3,w4.〈w1.w2〉 ≠ 〈w3.w4〉 → w1 ≠ w3 ∨ w2 ≠ w4.
#w1; #w2; #w3; #w4;
nnormalize; #H;
- napply (or_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (or_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
- ##[ ##2: #H2; napply (or_intror … H2)
+ napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
+ ##[ ##2: #H2; napply (or2_intro2 … H2)
##| ##1: #H2; nrewrite > H1 in H:(%);
nrewrite > H2;
#H; nelim (H (refl_eq …))
nelim dw1; #w1; #w2;
nelim dw2; #w3; #w4;
#H; nchange with (((eq_w16 w1 w3) ⊗ (eq_w16 w2 w4)) = false);
- napply (or_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …);
+ napply (or2_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …);
##[ ##1: #H1; nrewrite > (neq_to_neqw16 … H1); nnormalize; napply refl_eq
##| ##2: #H1; nrewrite > (neq_to_neqw16 … H1);
nrewrite > (symmetric_andbool (eq_w16 w1 w3) false);