nelim dw2;
#w3; #w4;
nchange with (
- match plus_w16_dc_dc w2 w4 c with
- [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
- match plus_w16_dc_dc w4 w2 c with
- [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
+ match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
+ match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
ncases (plus_w16_dc_dc w2 w4 c);
#w5; #c1;
nchange with (
- match plus_w16_dc_dc w1 w3 c1 with
- [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
- match plus_w16_dc_dc w3 w1 c1 with
- [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
+ match plus_w16_dc_dc w1 w3 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
+ match plus_w16_dc_dc w3 w1 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
nrewrite > (symmetric_plusw16_dc_dc w1 w3 c1);
napply refl_eq.
nqed.
nelim dw2;
#w3; #w4;
nchange with (
- match plus_w16_dc_dc w2 w4 c with
- [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
- match plus_w16_dc_dc w4 w2 c with
- [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
+ match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
+ match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
ncases (plus_w16_dc_dc w2 w4 c);
#w5; #c1;
nelim dw2;
#w3; #w4;
nchange with (
- match plus_w16_d_dc w2 w4 with
- [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
- match plus_w16_d_dc w4 w2 with
- [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
+ match plus_w16_d_dc w2 w4 with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
+ match plus_w16_d_dc w4 w2 with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
nrewrite > (symmetric_plusw16_d_dc w4 w2);
ncases (plus_w16_d_dc w2 w4);
#w5; #c;
nchange with (
- match plus_w16_dc_dc w1 w3 c with
- [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
- match plus_w16_dc_dc w3 w1 c with
- [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
+ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
+ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
nrewrite > (symmetric_plusw16_dc_dc w1 w3 c);
napply refl_eq.
nqed.
nelim dw2;
#w3; #w4;
nchange with (
- match plus_w16_d_dc w2 w4 with
- [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
- match plus_w16_d_dc w4 w2 with
- [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
+ match plus_w16_d_dc w2 w4 with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
+ match plus_w16_d_dc w4 w2 with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
nrewrite > (symmetric_plusw16_d_dc w4 w2);
ncases (plus_w16_d_dc w2 w4);
#w5; #c;
#w1; #w2; #w3; #w4;
nchange with ((((eq_w16 w3 w1) ⊗ (eq_w16 w4 w2)) = false) → ?);
#H;
- napply (or2_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_false2 … H) …);
##[ ##1: #H1; napply (decidable_w32_aux1 … (neqw16_to_neq … H1))
##| ##2: #H1; napply (decidable_w32_aux2 … (neqw16_to_neq … H1))
##]