X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fstatus_lemmas.ma;h=0be7272dbaf48ba9da00e4682636e57bee5e0946;hb=bf0cc84dcef9ae3d2145e79754bb39feb3985574;hp=806e140ba86004dca5c312e77a80c1f22b751ed5;hpb=f538a0b46ba4164a21a76e47a6ed3b3e9deb5041;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma index 806e140ba..0be7272db 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/status_lemmas.ma @@ -15,16 +15,16 @@ (* ********************************************************************** *) (* Progetto FreeScale *) (* *) -(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Ultima modifica: 05/08/2009 *) (* *) (* ********************************************************************** *) -include "freescale/word16_lemmas.ma". +include "num/word16_lemmas.ma". include "freescale/opcode_base_lemmas1.ma". include "freescale/status.ma". -include "freescale/option_lemmas.ma". -include "freescale/prod_lemmas.ma". +include "common/option_lemmas.ma". +include "common/prod_lemmas.ma". (* *********************************** *) (* STATUS INTERNO DEL PROCESSORE (ALU) *) @@ -199,7 +199,7 @@ nlemma aluHC05_destruct_13 : napply refl_eq. nqed. -nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05. +nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_aluHC05. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; @@ -229,7 +229,7 @@ nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05. napply refl_eq. nqed. -nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = alu2. +nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_aluHC05 alu1 alu2 = true → alu1 = alu2. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; @@ -270,7 +270,7 @@ nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = al napply refl_eq. nqed. -nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = true. +nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_aluHC05 alu1 alu2 = true. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; @@ -313,6 +313,198 @@ nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = tr napply refl_eq. nqed. +nlemma decidable_aluHC05_aux1 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x1 ≠ y1) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_1 … H1)). +nqed. + +nlemma decidable_aluHC05_aux2 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x2 ≠ y2) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_2 … H1)). +nqed. + +nlemma decidable_aluHC05_aux3 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x3 ≠ y3) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_3 … H1)). +nqed. + +nlemma decidable_aluHC05_aux4 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x4 ≠ y4) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_4 … H1)). +nqed. + +nlemma decidable_aluHC05_aux5 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x5 ≠ y5) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_5 … H1)). +nqed. + +nlemma decidable_aluHC05_aux6 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x6 ≠ y6) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_6 … H1)). +nqed. + +nlemma decidable_aluHC05_aux7 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x7 ≠ y7) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_7 … H1)). +nqed. + +nlemma decidable_aluHC05_aux8 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x8 ≠ y8) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_8 … H1)). +nqed. + +nlemma decidable_aluHC05_aux9 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x9 ≠ y9) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_9 … H1)). +nqed. + +nlemma decidable_aluHC05_aux10 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x10 ≠ y10) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_10 … H1)). +nqed. + +nlemma decidable_aluHC05_aux11 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x11 ≠ y11) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_11 … H1)). +nqed. + +nlemma decidable_aluHC05_aux12 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x12 ≠ y12) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_12 … H1)). +nqed. + +nlemma decidable_aluHC05_aux13 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13. + (x13 ≠ y13) → + (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠ + (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; #H; #H1; + napply (H (aluHC05_destruct_13 … H1)). +nqed. + +nlemma decidable_aluHC05 : ∀x,y:alu_HC05.decidable (x = y). + #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; + #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; + nnormalize; + napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …); + ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC05_aux1 … H)) + ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …); + ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC05_aux2 … H1)) + ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …); + ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC05_aux3 … H2)) + ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …); + ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC05_aux4 … H3)) + ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …); + ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC05_aux5 … H4)) + ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x6 y6) …); + ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC05_aux6 … H5)) + ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x7 y7) …); + ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC05_aux7 … H6)) + ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …); + ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC05_aux8 … H7)) + ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …); + ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC05_aux9 … H8)) + ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …); + ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC05_aux10 … H9)) + ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …); + ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC05_aux11 … H10)) + ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …); + ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC05_aux12 … H11)) + ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x13 y13) …); + ##[ ##2: #H12; napply (or2_intro2 … (decidable_aluHC05_aux13 … H12)) + ##| ##1: #H12; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3; + nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7; + nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11; + nrewrite > H12; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] +nqed. + nlemma aluHC08_destruct_1 : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 → @@ -469,7 +661,7 @@ nlemma aluHC08_destruct_12 : napply refl_eq. nqed. -nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08. +nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_aluHC08. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; @@ -497,7 +689,7 @@ nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08. napply refl_eq. nqed. -nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = alu2. +nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_aluHC08 alu1 alu2 = true → alu1 = alu2. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; @@ -532,7 +724,7 @@ nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = al napply refl_eq. nqed. -nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = true. +nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_aluHC08 alu1 alu2 = true. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; @@ -569,6 +761,184 @@ nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = tr napply refl_eq. nqed. +nlemma decidable_aluHC08_aux1 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x1 ≠ y1) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_1 … H1)). +nqed. + +nlemma decidable_aluHC08_aux2 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x2 ≠ y2) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_2 … H1)). +nqed. + +nlemma decidable_aluHC08_aux3 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x3 ≠ y3) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_3 … H1)). +nqed. + +nlemma decidable_aluHC08_aux4 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x4 ≠ y4) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_4 … H1)). +nqed. + +nlemma decidable_aluHC08_aux5 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x5 ≠ y5) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_5 … H1)). +nqed. + +nlemma decidable_aluHC08_aux6 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x6 ≠ y6) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_6 … H1)). +nqed. + +nlemma decidable_aluHC08_aux7 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x7 ≠ y7) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_7 … H1)). +nqed. + +nlemma decidable_aluHC08_aux8 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x8 ≠ y8) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_8 … H1)). +nqed. + +nlemma decidable_aluHC08_aux9 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x9 ≠ y9) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_9 … H1)). +nqed. + +nlemma decidable_aluHC08_aux10 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x10 ≠ y10) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_10 … H1)). +nqed. + +nlemma decidable_aluHC08_aux11 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x11 ≠ y11) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_11 … H1)). +nqed. + +nlemma decidable_aluHC08_aux12 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12. + (x12 ≠ y12) → + (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠ + (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; #H; #H1; + napply (H (aluHC08_destruct_12 … H1)). +nqed. + +nlemma decidable_aluHC08 : ∀x,y:alu_HC08.decidable (x = y). + #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; + #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; + nnormalize; + napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …); + ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC08_aux1 … H)) + ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …); + ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC08_aux2 … H1)) + ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x3 y3) …); + ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC08_aux3 … H2)) + ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …); + ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC08_aux4 … H3)) + ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …); + ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC08_aux5 … H4)) + ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x6 y6) …); + ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC08_aux6 … H5)) + ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …); + ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC08_aux7 … H6)) + ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …); + ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC08_aux8 … H7)) + ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …); + ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC08_aux9 … H8)) + ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …); + ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC08_aux10 … H9)) + ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …); + ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC08_aux11 … H10)) + ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …); + ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC08_aux12 … H11)) + ##| ##1: #H11; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3; + nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7; + nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11; + napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] +nqed. + nlemma aluRS08_destruct_1 : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 → @@ -673,7 +1043,7 @@ nlemma aluRS08_destruct_8 : napply refl_eq. nqed. -nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08. +nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_aluRS08. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; @@ -699,7 +1069,7 @@ nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08. napply refl_eq. nqed. -nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = alu2. +nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_aluRS08 alu1 alu2 = true → alu1 = alu2. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; @@ -727,7 +1097,7 @@ nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = al napply refl_eq. nqed. -nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = true. +nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_aluRS08 alu1 alu2 = true. #alu1; #alu2; ncases alu1; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; @@ -757,6 +1127,127 @@ nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = tr napply refl_eq. nqed. +nlemma decidable_aluRS08_aux1 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. + (x1 ≠ y1) → + (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠ + (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; #H; #H1; + napply (H (aluRS08_destruct_1 … H1)). +nqed. + +nlemma decidable_aluRS08_aux2 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. + (x2 ≠ y2) → + (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠ + (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; #H; #H1; + napply (H (aluRS08_destruct_2 … H1)). +nqed. + +nlemma decidable_aluRS08_aux3 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. + (x3 ≠ y3) → + (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠ + (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; #H; #H1; + napply (H (aluRS08_destruct_3 … H1)). +nqed. + +nlemma decidable_aluRS08_aux4 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. + (x4 ≠ y4) → + (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠ + (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; #H; #H1; + napply (H (aluRS08_destruct_4 … H1)). +nqed. + +nlemma decidable_aluRS08_aux5 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. + (x5 ≠ y5) → + (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠ + (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; #H; #H1; + napply (H (aluRS08_destruct_5 … H1)). +nqed. + +nlemma decidable_aluRS08_aux6 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. + (x6 ≠ y6) → + (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠ + (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; #H; #H1; + napply (H (aluRS08_destruct_6 … H1)). +nqed. + +nlemma decidable_aluRS08_aux7 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. + (x7 ≠ y7) → + (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠ + (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; #H; #H1; + napply (H (aluRS08_destruct_7 … H1)). +nqed. + +nlemma decidable_aluRS08_aux8 + : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8. + (x8 ≠ y8) → + (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠ + (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8). + #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; #H; #H1; + napply (H (aluRS08_destruct_8 … H1)). +nqed. + +nlemma decidable_aluRS08 : ∀x,y:alu_RS08.decidable (x = y). + #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; + #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; + nnormalize; + napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …); + ##[ ##2: #H; napply (or2_intro2 … (decidable_aluRS08_aux1 … H)) + ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x2 y2) …); + ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluRS08_aux2 … H1)) + ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …); + ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluRS08_aux3 … H2)) + ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …); + ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluRS08_aux4 … H3)) + ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x5 y5) …); + ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluRS08_aux5 … H4)) + ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x6 y6) …); + ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluRS08_aux6 … H5)) + ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …); + ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluRS08_aux7 … H6)) + ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …); + ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluRS08_aux8 … H7)) + ##| ##1: #H7; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3; + nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7; + napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …)) + ##] + ##] + ##] + ##] + ##] + ##] + ##] + ##] +nqed. + nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1. #mcu; #clk1; #clk2; ncases clk1; @@ -766,11 +1257,11 @@ nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5; #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; nchange with ( - ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = - ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_instrmode x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5))); + ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = + ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_im x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5))); nrewrite > (symmetric_eqb8 x1 y1); nrewrite > (symmetric_eqanyop ? x2 y2); - nrewrite > (symmetric_eqinstrmode x3 y3); + nrewrite > (symmetric_eqim x3 y3); nrewrite > (symmetric_eqb8 x4 y4); nrewrite > (symmetric_eqw16 x5 y5); napply refl_eq @@ -786,12 +1277,12 @@ nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5; #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H; nchange in H:(%) with ( - ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true); + ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true); nrewrite > (eqw16_to_eq … (andb_true_true_r … H)); nletin H1 ≝ (andb_true_true_l … H); nrewrite > (eqb8_to_eq … (andb_true_true_r … H1)); nletin H2 ≝ (andb_true_true_l … H1); - nrewrite > (eqinstrmode_to_eq … (andb_true_true_r … H2)); + nrewrite > (eqim_to_eq … (andb_true_true_r … H2)); nletin H3 ≝ (andb_true_true_l … H2); nrewrite > (eqanyop_to_eq … (andb_true_true_r … H3)); nrewrite > (eqb8_to_eq … (andb_true_true_l … H3)); @@ -804,8 +1295,8 @@ nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = tru ncases clk1; ncases clk2; ##[ ##1: nnormalize; #H; napply refl_eq - ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some … H1) - ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none … H1) + ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ? p … H1) + ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ? p … H1) ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5; #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H; nrewrite > (quintuple_destruct_1 … (option_destruct_some_some … H)); @@ -814,10 +1305,10 @@ nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = tru nrewrite > (quintuple_destruct_4 … (option_destruct_some_some … H)); nrewrite > (quintuple_destruct_5 … (option_destruct_some_some … H)); nchange with ( - ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_instrmode x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true); + ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_im x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true); nrewrite > (eq_to_eqb8 x1 x1 (refl_eq …)); nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2)); - nrewrite > (eq_to_eqinstrmode x3 x3 (refl_eq …)); + nrewrite > (eq_to_eqim x3 x3 (refl_eq …)); nrewrite > (eq_to_eqb8 x4 x4 (refl_eq …)); nrewrite > (eq_to_eqw16 x5 x5 (refl_eq …)); nnormalize; @@ -902,28 +1393,28 @@ nlemma anystatus_destruct_4 : napply refl_eq. nqed. -nlemma symmetric_eqstatus : +nlemma symmetric_eqanystatus : ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t. - eq_status m t s1 s2 addrl = eq_status m t s2 s1 addrl. + eq_anystatus m t s1 s2 addrl = eq_anystatus m t s2 s1 addrl. #addrl; #m; ncases m; #t; #s1; ##[ ##1: ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; nchange with ( - ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) = - ((eq_alu_HC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4))); + ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) = + ((eq_aluHC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4))); nrewrite > (symmetric_eqaluHC05 x1 y1) ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; nchange with ( - ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = - ((eq_alu_HC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4))); + ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = + ((eq_aluHC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4))); nrewrite > (symmetric_eqaluHC08 x1 y1) ##| ##4: ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; nchange with ( - ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) = - ((eq_alu_RS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4))); + ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) = + ((eq_aluRS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4))); nrewrite > (symmetric_eqaluRS08 x1 y1) ##] nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl); @@ -931,58 +1422,58 @@ nlemma symmetric_eqstatus : napply refl_eq. nqed. -nlemma eqstatus_to_eq : +nlemma eqanystatus_to_eq : ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t. - (eq_status m t s1 s2 addrl = true) → - ((alu m t s1 = alu m t s2) ∧ - (clk_desc m t s1 = clk_desc m t s2) ∧ - ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2) - (mem_desc m t s1) (mem_desc m t s2) addrl) = true)). + (eq_anystatus m t s1 s2 addrl = true) → + And3 (alu m t s1 = alu m t s2) + (clk_desc m t s1 = clk_desc m t s2) + ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2) + (mem_desc m t s1) (mem_desc m t s2) addrl) = true). #addrl; #m; #t; ncases m; #s1; ##[ ##1: ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; nchange in H:(%) with ( - ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nrewrite > (eqaluHC05_to_eq … (andb_true_true_l … (andb_true_true_l … H))) ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; nchange in H:(%) with ( - ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nrewrite > (eqaluHC08_to_eq … (andb_true_true_l … (andb_true_true_l … H))) ##| ##4: ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; nchange in H:(%) with ( - ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nrewrite > (eqaluRS08_to_eq … (andb_true_true_l … (andb_true_true_l … H))) ##] - nchange with ((y1 = y1) ∧ (x4 = y4) ∧ (forall_memory_ranged t x3 y3 x2 y2 addrl = true)); + nchange with (And3 (y1 = y1) (x4 = y4) (forall_memory_ranged t x3 y3 x2 y2 addrl = true)); nrewrite > (andb_true_true_r … (andb_true_true_l … H)); nrewrite > (eqclk_to_eq … (andb_true_true_r … H)); - napply (conj … (conj … (refl_eq …) (refl_eq …)) (refl_eq …)). + napply (conj3 … (refl_eq ? y1) (refl_eq ? y4) (refl_eq ? true)). nqed. -nlemma eq_to_eqstatus_strong : +nlemma eq_to_eqanystatus_strong : ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t. - s1 = s2 → (eq_status m t s1 s2 addrl = true). + s1 = s2 → (eq_anystatus m t s1 s2 addrl = true). #addrl; #m; #t; ncases m; ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; nchange with ( - ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nrewrite > (anystatus_destruct_1 … H); nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …)) ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; nchange with ( - ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nrewrite > (anystatus_destruct_1 … H); nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …)) ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; nchange with ( - ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nrewrite > (anystatus_destruct_1 … H); nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …)) ##] @@ -992,7 +1483,7 @@ nlemma eq_to_eqstatus_strong : nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …)); nchange with ((forall_memory_ranged … ⊗ true) =true); nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true); - nchange with (forall_memory_ranged … = true); + nchange with ((forall_memory_ranged t y3 y3 y2 y2 ?) = true); napply (list_ind word16 … addrl); ##[ ##1,3,5,7: nnormalize; napply refl_eq ##| ##2,4,6,8: #a; #l'; #H; @@ -1007,30 +1498,30 @@ nlemma eq_to_eqstatus_strong : ##] nqed. -nlemma eq_to_eqstatus_weak : +nlemma eq_to_eqanystatus_weak : ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t. (alu m t s1 = alu m t s2) → (clk_desc m t s1 = clk_desc m t s2) → ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2) (mem_desc m t s1) (mem_desc m t s2) addrl) = true) → - (eq_status m t s1 s2 addrl = true). + (eq_anystatus m t s1 s2 addrl = true). #addrl; #m; #t; ncases m; ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2; - nchange with (((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + nchange with (((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nchange in H:(%) with (x1 = y1); nrewrite > H; nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …)) ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2; - nchange with (((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + nchange with (((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nchange in H:(%) with (x1 = y1); nrewrite > H; nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …)) ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4; #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2; - nchange with (((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); + nchange with (((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true); nchange in H:(%) with (x1 = y1); nrewrite > H; nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))