nlemma decidable_ascii1 : ∀x:ascii.decidable (ch_0 = x).
#x; nnormalize; nelim x;
- ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii2 : ∀x:ascii.decidable (ch_1 = x).
#x; nnormalize; nelim x;
- ##[ ##2: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii3 : ∀x:ascii.decidable (ch_2 = x).
#x; nnormalize; nelim x;
- ##[ ##3: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii4 : ∀x:ascii.decidable (ch_3 = x).
#x; nnormalize; nelim x;
- ##[ ##4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii5 : ∀x:ascii.decidable (ch_4 = x).
#x; nnormalize; nelim x;
- ##[ ##5: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii6 : ∀x:ascii.decidable (ch_5 = x).
#x; nnormalize; nelim x;
- ##[ ##6: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii7 : ∀x:ascii.decidable (ch_6 = x).
#x; nnormalize; nelim x;
- ##[ ##7: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii8 : ∀x:ascii.decidable (ch_7 = x).
#x; nnormalize; nelim x;
- ##[ ##8: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii9 : ∀x:ascii.decidable (ch_8 = x).
#x; nnormalize; nelim x;
- ##[ ##9: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii10 : ∀x:ascii.decidable (ch_9 = x).
#x; nnormalize; nelim x;
- ##[ ##10: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii11 : ∀x:ascii.decidable (ch__ = x).
#x; nnormalize; nelim x;
- ##[ ##11: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii12 : ∀x:ascii.decidable (ch_A = x).
#x; nnormalize; nelim x;
- ##[ ##12: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii13 : ∀x:ascii.decidable (ch_B = x).
#x; nnormalize; nelim x;
- ##[ ##13: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii14 : ∀x:ascii.decidable (ch_C = x).
#x; nnormalize; nelim x;
- ##[ ##14: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii15 : ∀x:ascii.decidable (ch_D = x).
#x; nnormalize; nelim x;
- ##[ ##15: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii16 : ∀x:ascii.decidable (ch_E = x).
#x; nnormalize; nelim x;
- ##[ ##16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii17 : ∀x:ascii.decidable (ch_F = x).
#x; nnormalize; nelim x;
- ##[ ##17: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii18 : ∀x:ascii.decidable (ch_G = x).
#x; nnormalize; nelim x;
- ##[ ##18: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii19 : ∀x:ascii.decidable (ch_H = x).
#x; nnormalize; nelim x;
- ##[ ##19: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii20 : ∀x:ascii.decidable (ch_I = x).
#x; nnormalize; nelim x;
- ##[ ##20: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii21 : ∀x:ascii.decidable (ch_J = x).
#x; nnormalize; nelim x;
- ##[ ##21: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii22 : ∀x:ascii.decidable (ch_K = x).
#x; nnormalize; nelim x;
- ##[ ##22: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii23 : ∀x:ascii.decidable (ch_L = x).
#x; nnormalize; nelim x;
- ##[ ##23: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii24 : ∀x:ascii.decidable (ch_M = x).
#x; nnormalize; nelim x;
- ##[ ##24: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii25 : ∀x:ascii.decidable (ch_N = x).
#x; nnormalize; nelim x;
- ##[ ##25: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii26 : ∀x:ascii.decidable (ch_O = x).
#x; nnormalize; nelim x;
- ##[ ##26: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii27 : ∀x:ascii.decidable (ch_P = x).
#x; nnormalize; nelim x;
- ##[ ##27: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii28 : ∀x:ascii.decidable (ch_Q = x).
#x; nnormalize; nelim x;
- ##[ ##28: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii29 : ∀x:ascii.decidable (ch_R = x).
#x; nnormalize; nelim x;
- ##[ ##29: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii30 : ∀x:ascii.decidable (ch_S = x).
#x; nnormalize; nelim x;
- ##[ ##30: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii31 : ∀x:ascii.decidable (ch_T = x).
#x; nnormalize; nelim x;
- ##[ ##31: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii32 : ∀x:ascii.decidable (ch_U = x).
#x; nnormalize; nelim x;
- ##[ ##32: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii33 : ∀x:ascii.decidable (ch_V = x).
#x; nnormalize; nelim x;
- ##[ ##33: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##33: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii34 : ∀x:ascii.decidable (ch_W = x).
#x; nnormalize; nelim x;
- ##[ ##34: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##34: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii35 : ∀x:ascii.decidable (ch_X = x).
#x; nnormalize; nelim x;
- ##[ ##35: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##35: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii36 : ∀x:ascii.decidable (ch_Y = x).
#x; nnormalize; nelim x;
- ##[ ##36: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##36: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii37 : ∀x:ascii.decidable (ch_Z = x).
#x; nnormalize; nelim x;
- ##[ ##37: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##37: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii38 : ∀x:ascii.decidable (ch_a = x).
#x; nnormalize; nelim x;
- ##[ ##38: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##38: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii39 : ∀x:ascii.decidable (ch_b = x).
#x; nnormalize; nelim x;
- ##[ ##39: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##39: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii40 : ∀x:ascii.decidable (ch_c = x).
#x; nnormalize; nelim x;
- ##[ ##40: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##40: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii41 : ∀x:ascii.decidable (ch_d = x).
#x; nnormalize; nelim x;
- ##[ ##41: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##41: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii42 : ∀x:ascii.decidable (ch_e = x).
#x; nnormalize; nelim x;
- ##[ ##42: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##42: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii43 : ∀x:ascii.decidable (ch_f = x).
#x; nnormalize; nelim x;
- ##[ ##43: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##43: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii44 : ∀x:ascii.decidable (ch_g = x).
#x; nnormalize; nelim x;
- ##[ ##44: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##44: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii45 : ∀x:ascii.decidable (ch_h = x).
#x; nnormalize; nelim x;
- ##[ ##45: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##45: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii46 : ∀x:ascii.decidable (ch_i = x).
#x; nnormalize; nelim x;
- ##[ ##46: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##46: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii47 : ∀x:ascii.decidable (ch_j = x).
#x; nnormalize; nelim x;
- ##[ ##47: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##47: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii48 : ∀x:ascii.decidable (ch_k = x).
#x; nnormalize; nelim x;
- ##[ ##48: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##48: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii49 : ∀x:ascii.decidable (ch_l = x).
#x; nnormalize; nelim x;
- ##[ ##49: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##49: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii50 : ∀x:ascii.decidable (ch_m = x).
#x; nnormalize; nelim x;
- ##[ ##50: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##50: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii51 : ∀x:ascii.decidable (ch_n = x).
#x; nnormalize; nelim x;
- ##[ ##51: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##51: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii52 : ∀x:ascii.decidable (ch_o = x).
#x; nnormalize; nelim x;
- ##[ ##52: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##52: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii53 : ∀x:ascii.decidable (ch_p = x).
#x; nnormalize; nelim x;
- ##[ ##53: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##53: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii54 : ∀x:ascii.decidable (ch_q = x).
#x; nnormalize; nelim x;
- ##[ ##54: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##54: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii55 : ∀x:ascii.decidable (ch_r = x).
#x; nnormalize; nelim x;
- ##[ ##55: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##55: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii56 : ∀x:ascii.decidable (ch_s = x).
#x; nnormalize; nelim x;
- ##[ ##56: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##56: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii57 : ∀x:ascii.decidable (ch_t = x).
#x; nnormalize; nelim x;
- ##[ ##57: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##57: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii58 : ∀x:ascii.decidable (ch_u = x).
#x; nnormalize; nelim x;
- ##[ ##58: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##58: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii59 : ∀x:ascii.decidable (ch_v = x).
#x; nnormalize; nelim x;
- ##[ ##59: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##59: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii60 : ∀x:ascii.decidable (ch_w = x).
#x; nnormalize; nelim x;
- ##[ ##60: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##60: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii61 : ∀x:ascii.decidable (ch_x = x).
#x; nnormalize; nelim x;
- ##[ ##61: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##61: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii62 : ∀x:ascii.decidable (ch_y = x).
#x; nnormalize; nelim x;
- ##[ ##62: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##62: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
nlemma decidable_ascii63 : ∀x:ascii.decidable (ch_z = x).
#x; nnormalize; nelim x;
- ##[ ##63: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
+ ##[ ##63: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (ascii_destruct … H)
##]
nqed.
##]
nqed.
+nlemma bfoldrightlist2_to_lenlist
+ : ∀T.∀f:T → T → bool.∀l1,l2:list T.bfold_right_list2 T f l1 l2 = true → len_list T l1 = len_list T l2.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+ ##[ ##1: nnormalize; #H; napply refl_eq
+ ##| ##2: nnormalize; #hh; #tt; #H; napply (bool_destruct … H)
+ ##]
+ ##| ##2: #hh; #tt; #H; #l2; ncases l2;
+ ##[ ##1: nnormalize; #H1; napply (bool_destruct … H1)
+ ##| ##2: #hh1; #tt1; #H1; nnormalize;
+ nrewrite > (H tt1 ?);
+ ##[ ##1: napply refl_eq
+ ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true);
+ napply (andb_true_true_r … H1)
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma decidable_list : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:list T.decidable (x = y).
+ #T; #H; #x; nelim x;
+ ##[ ##1: #y; ncases y;
+ ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H1; napply (list_destruct_nil_cons T … H1)
+ ##]
+ ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
+ ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H2; napply (list_destruct_cons_nil T … H2)
+ ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
+ ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
+ ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
+ ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H4; napply (H3 (list_destruct_2 T … H4))
+ ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ nrewrite > H2; nrewrite > H3; napply refl_eq
+ ##]
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma nbfoldrightlist2_to_neq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
+ (∀x,y.(f x y = false → x ≠ y)) →
+ (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+ ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
+ ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #H1; #H2; nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
+ ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
+ nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
+ napply (H ll2 H1 ? (list_destruct_2 T … H3));
+ napply (or2_elim ??? (andb_false … H2) );
+ ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
+ ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
+ ##| ##2: napply (H1 … H4)
+ ##]
+ ##| ##2: #H4; napply H4
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma list_destruct
+ : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:list T.(h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2.
+ #T; #H; #h1; #h2; #l1; nelim l1;
+ ##[ ##1: #l2; ncases l2;
+ ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …);
+ nnormalize; #H2; nrewrite > H2 in H1:(%);
+ nnormalize; #H1; napply (H1 (refl_eq …))
+ ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
+ nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
+ ##]
+ ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
+ ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
+ nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
+ ##| ##2: #hh2; #ll2; #H2;
+ napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
+ ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
+ ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …));
+ nrewrite > H3 in H2:(%); #H2;
+ nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2;
+ nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2;
+ napply (H2 (refl_eq …))
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_nbfoldrightlist2
+ : ∀T:Type.∀f:T → T → bool.∀l1,l2:list T.
+ (∀x,y:T.decidable (x = y)) →
+ (∀x,y.(x ≠ y → f x y = false)) →
+ (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #l2; ncases l2;
+ ##[ ##1: #H; #H1; nnormalize; #H2; nelim (H2 (refl_eq …))
+ ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #H1; #H2; nnormalize; #H3; napply refl_eq
+ ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
+ nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
+ napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H1 … H3) …);
+ ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
+ ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
+ nrewrite > (symmetric_andbool (f hh1 hh2) false);
+ nnormalize; napply refl_eq
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
+ #T; #l;
+ ncases l;
+ nnormalize;
+ ##[ ##1: #H; napply I
+ ##| ##2: #x; #l; #H; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
+ #T; #l;
+ ncases l;
+ nnormalize;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##2: #x; #l; #H; napply I
+ ##]
+nqed.
+
(* ************** *)
(* NON-EMPTY LIST *)
(* ************** *)
##]
nqed.
-nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
- #T; #l;
- ncases l;
- nnormalize;
- ##[ ##1: #H; napply I
- ##| ##2: #x; #l; #H; napply (bool_destruct … H)
+nlemma bfoldrightnelist2_to_lennelist
+ : ∀T.∀f:T → T → bool.∀l1,l2:ne_list T.bfold_right_neList2 T f l1 l2 = true → len_neList T l1 = len_neList T l2.
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+ ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
+ ##| ##2: nnormalize; #hh2; #tt2; #H; napply (bool_destruct … H)
+ ##]
+ ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
+ ##[ ##1: nnormalize; #hh2; #H1; napply (bool_destruct … H1)
+ ##| ##2: #hh2; #tt2; #H1; nnormalize;
+ nrewrite > (H tt2 ?);
+ ##[ ##1: napply refl_eq
+ ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true);
+ napply (andb_true_true_r … H1)
+ ##]
+ ##]
##]
nqed.
-nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
- #T; #l;
- ncases l;
- nnormalize;
- ##[ ##1: #H; napply (bool_destruct … H)
- ##| ##2: #x; #l; #H; napply I
+nlemma decidable_nelist : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:ne_list T.decidable (x = y).
+ #T; #H; #x; nelim x;
+ ##[ ##1: #hh1; #y; ncases y;
+ ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2));
+ ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize;
+ #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
+ ##]
+ ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H1; napply (nelist_destruct_nil_cons T … H1)
+ ##]
+ ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
+ ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H2; napply (nelist_destruct_cons_nil T … H2)
+ ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
+ ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
+ ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
+ ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4))
+ ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ nrewrite > H2; nrewrite > H3; napply refl_eq
+ ##]
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma nbfoldrightnelist2_to_neq
+ : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
+ (∀x,y.(f x y = false → x ≠ y)) →
+ (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+ ##[ ##1: #hh2; #H; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
+ ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
+ ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
+ nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
+ napply (H ll2 H1 ? (nelist_destruct_cons_cons_2 T … H3));
+ napply (or2_elim ??? (andb_false … H2) );
+ ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
+ ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
+ ##| ##2: napply (H1 … H4)
+ ##]
+ ##| ##2: #H4; napply H4
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma nelist_destruct
+ : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:ne_list T.(h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2.
+ #T; #H; #h1; #h2; #l1; nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+ ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …);
+ ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2)
+ ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1;
+ napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …);
+ ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?);
+ nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4))
+ ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …))
+ ##]
+ ##]
+ ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
+ nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
+ ##]
+ ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
+ ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
+ nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
+ ##| ##2: #hh2; #ll2; #H2;
+ napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
+ ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3)
+ ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2) …));
+ nrewrite > H3 in H2:(%); #H2;
+ nnormalize; #H4; nrewrite > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2;
+ nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2;
+ napply (H2 (refl_eq …))
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_nbfoldrightnelist2
+ : ∀T:Type.∀f:T → T → bool.∀l1,l2:ne_list T.
+ (∀x,y:T.decidable (x = y)) →
+ (∀x,y.(x ≠ y → f x y = false)) →
+ (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false).
+ #T; #f; #l1;
+ nelim l1;
+ ##[ ##1: #hh1; #l2; ncases l2;
+ ##[ ##1: #hh2; #H; #H1; nnormalize; #H2; napply (H1 hh1 hh2 ?);
+ nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …))
+ ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
+ ##]
+ ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
+ ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply refl_eq
+ ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
+ nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
+ napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H1 … H3) …);
+ ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
+ ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
+ nrewrite > (symmetric_andbool (f hh1 hh2) false);
+ nnormalize; napply refl_eq
+ ##]
+ ##]
##]
nqed.
napply (H n4 (nat_destruct_S_S … H1))
##]
##]
-nqed.
+nqed.
nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
#n1;
##]
nqed.
+nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
+ #x; nelim x; nnormalize;
+ ##[ ##1: #y; ncases y;
+ ##[ ##1: napply (or2_intro1 (O = O) (O ≠ O) (refl_eq …))
+ ##| ##2: #n2; napply (or2_intro2 (O = (S n2)) (O ≠ (S n2)) ?);
+ nnormalize; #H; napply (nat_destruct_0_S n2 H)
+ ##]
+ ##| ##2: #n1; #H; #y; ncases y;
+ ##[ ##1: napply (or2_intro2 ((S n1) = O) ((S n1) ≠ O) ?);
+ nnormalize; #H1; napply (nat_destruct_S_0 n1 H1)
+ ##| ##2: #n2; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (H n2) …);
+ ##[ ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) …);
+ nrewrite > H1; napply refl_eq
+ ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …);
+ nnormalize; #H2; napply (H1 (nat_destruct_S_S … H2))
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
+ #n1; nelim n1;
+ ##[ ##1: #n2; ncases n2;
+ ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
+ ##| ##2: #nn2; #H; nnormalize; napply refl_eq
+ ##]
+ ##| ##2: #nn1; #H; #n2; ncases n2;
+ ##[ ##1: #H1; nnormalize; napply refl_eq
+ ##| ##2: #nn2; nnormalize; #H1;
+ napply (H nn2 ?); nnormalize; #H2;
+ nrewrite > H2 in H1:(%); #H1;
+ napply (H1 (refl_eq …))
+ ##]
+ ##]
+nqed.
+
+nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
+ #n1; nelim n1;
+ ##[ ##1: #n2; ncases n2;
+ ##[ ##1: nnormalize; #H; napply (bool_destruct … H)
+ ##| ##2: #nn2; nnormalize; #H; #H1; nelim (nat_destruct_0_S … H1)
+ ##]
+ ##| ##2: #nn1; #H; #n2; ncases n2;
+ ##[ ##1: nnormalize; #H1; #H2; nelim (nat_destruct_S_0 … H2)
+ ##| ##2: #nn2; nnormalize; #H1; #H2; napply (H nn2 H1 ?);
+ napply (nat_destruct_S_S … H2)
+ ##]
+ ##]
+nqed.
+
nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
#n1;
nelim n1;
napply refl_eq
##]
nqed.
+
+nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T.decidable (x = y).
+ #T; #H; #x; nelim x;
+ ##[ ##1: #y; ncases y;
+ ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
+ ##| ##2: #yy; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H1; napply (option_destruct_none_some T … H1)
+ ##]
+ ##| ##2: #xx; #y; ncases y;
+ ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H2; napply (option_destruct_some_none T … H2)
+ ##| ##2: #yy; nnormalize; napply (or2_elim (xx = yy) (xx ≠ yy) ? (H …));
+ ##[ ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H2; napply (H1 (option_destruct_some_some T … H2))
+ ##| ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ nrewrite > H1; napply refl_eq
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqoption :
+∀T.∀op1,op2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
+ (op1 ≠ op2 → eq_option T op1 op2 f = false).
+ #T; #op1; nelim op1;
+ ##[ ##1: #op2; ncases op2;
+ ##[ ##1: nnormalize; #f; #H; #H1; nelim (H1 (refl_eq …))
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; napply refl_eq
+ ##]
+ ##| ##2: #xx; #op2; ncases op2;
+ ##[ ##1: #f; #H; nnormalize; #H1; napply refl_eq
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; napply (H xx yy …);
+ nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
+ napply (H1 (refl_eq …))
+ ##]
+ ##]
+nqed.
+
+nlemma neqoption_to_neq :
+∀T.∀op1,op2:option T.∀f:T → T → bool.
+ (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
+ (eq_option T op1 op2 f = false → op1 ≠ op2).
+ #T; #op1; nelim op1;
+ ##[ ##1: #op2; ncases op2;
+ ##[ ##1: nnormalize; #f; #H; #H1; napply (bool_destruct … H1)
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (option_destruct_none_some T … H2)
+ ##]
+ ##| ##2: #xx; #op2; ncases op2;
+ ##[ ##1: nnormalize; #f; #H; #H1; #H2; napply (option_destruct_some_none T … H2)
+ ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
+ napply (option_destruct_some_some T … H2)
+ ##]
+ ##]
+nqed.
include "common/prod.ma".
include "num/bool_lemmas.ma".
-(* ***** *)
-(* TUPLE *)
-(* ***** *)
+(* ********* *)
+(* TUPLE x 2 *)
+(* ********* *)
nlemma pair_destruct_1 :
∀T1,T2.∀x1,x2:T1.∀y1,y2:T2.
nlemma eq_to_eqpair :
∀T1,T2.∀p1,p2:ProdT T1 T2.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
- (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
- (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
+ (∀x,y:T1.x = y → f1 x y = true) →
+ (∀x,y:T2.x = y → f2 x y = true) →
(p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
#T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
nelim p1;
nlemma eqpair_to_eq :
∀T1,T2.∀p1,p2:ProdT T1 T2.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
- (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
- (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
+ (∀x,y:T1.f1 x y = true → x = y) →
+ (∀x,y:T2.f2 x y = true → x = y) →
(eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
#T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
nelim p1;
napply refl_eq.
nqed.
+nlemma decidable_pair
+ : ∀T1,T2.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ ∀x,y:ProdT T1 T2.decidable (x = y).
+ #T1; #T2; #H; #H1;
+ #x; nelim x; #xx1; #xx2;
+ #y; nelim y; #yy1; #yy2;
+ nnormalize;
+ napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
+ ##[ ##1: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H3; napply (H2 (pair_destruct_1 T1 T2 … H3))
+ ##| ##2: #H2; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+ ##[ ##1: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H4; napply (H3 (pair_destruct_2 T1 T2 … H4))
+ ##| ##2: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ nrewrite > H2; nrewrite > H3; napply refl_eq
+ ##]
+ ##]
+nqed.
+
+nlemma neqpair_to_neq :
+ ∀T1,T2.∀p1,p2:ProdT T1 T2.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (∀x,y:T1.f1 x y = false → x ≠ y) →
+ (∀x,y:T2.f2 x y = false → x ≠ y) →
+ (eq_pair T1 T2 p1 p2 f1 f2 = false → p1 ≠ p2).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2;
+ nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2)) = false) → ?); #H;
+ nnormalize; #H3;
+ napply (or2_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ? (andb_false2 … H) ?);
+ ##[ ##1: #H4; napply (H2 y1 y2 H4); napply (pair_destruct_2 T1 T2 … H3)
+ ##| ##2: #H4; napply (H1 x1 x2 H4); napply (pair_destruct_1 T1 T2 … H3)
+ ##]
+nqed.
+
+nlemma pair_destruct
+ : ∀T1,T2.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ ∀x1,x2:T1.∀y1,y2:T2.(pair T1 T2 x1 y1) ≠ (pair T1 T2 x2 y2) → x1 ≠ x2 ∨ y1 ≠ y2.
+ #T1; #T2; #H1; #H2; #x1; #x2; #y1; #y2;
+ nnormalize; #H;
+ napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
+ ##[ ##1: #H3; napply (or2_intro1 … H3)
+ ##| ##2: #H3; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##1: #H4; napply (or2_intro2 … H4)
+ ##| ##2: #H4; nrewrite > H3 in H:(%);
+ nrewrite > H4; #H; nelim (H (refl_eq …))
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqpair :
+ ∀T1,T2.∀p1,p2:ProdT T1 T2.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T1.x ≠ y → f1 x y = false) →
+ (∀x,y:T2.x ≠ y → f2 x y = false) →
+ (p1 ≠ p2 → eq_pair T1 T2 p1 p2 f1 f2 = false).
+ #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1;
+ nelim p2;
+ #x2; #y2; #H;
+ nchange with (((f1 x1 x2) ⊗ (f2 y1 y2)) = false);
+ napply (or2_elim (x1 ≠ x2) (y1 ≠ y2) ? (pair_destruct T1 T2 H1 H2 … H) ?);
+ ##[ ##1: #H5; nrewrite > (H4 … H5); nrewrite > (andb_false2_2 (f1 x1 x2)); napply refl_eq
+ ##| ##2: #H5; nrewrite > (H3 … H5); nnormalize; napply refl_eq
+ ##]
+nqed.
+
+(* ********* *)
+(* TUPLE x 3 *)
+(* ********* *)
+
nlemma triple_destruct_1 :
∀T1,T2,T3.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.
triple T1 T2 T3 x1 y1 z1 = triple T1 T2 T3 x2 y2 z2 → x1 = x2.
napply refl_eq.
nqed.
+nlemma decidable_triple
+ : ∀T1,T2,T3.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ ∀x,y:Prod3T T1 T2 T3.decidable (x = y).
+ #T1; #T2; #T3; #H; #H1; #H2;
+ #x; nelim x; #xx1; #xx2; #xx3;
+ #y; nelim y; #yy1; #yy2; #yy3;
+ nnormalize;
+ napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
+ ##[ ##1: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H4; napply (H3 (triple_destruct_1 T1 T2 T3 … H4))
+ ##| ##2: #H3; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+ ##[ ##1: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H5; napply (H4 (triple_destruct_2 T1 T2 T3 … H5))
+ ##| ##2: #H4; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+ ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H6; napply (H5 (triple_destruct_3 T1 T2 T3 … H6))
+ ##| ##2: #H5; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ nrewrite > H3;
+ nrewrite > H4;
+ nrewrite > H5;
+ napply refl_eq
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neqtriple_to_neq :
+ ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (∀x,y:T1.f1 x y = false → x ≠ y) →
+ (∀x,y:T2.f2 x y = false → x ≠ y) →
+ (∀x,y:T3.f3 x y = false → x ≠ y) →
+ (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2;
+ nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false) → ?); #H;
+ nnormalize; #H4;
+ napply (or3_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ? (andb_false3 … H) ?);
+ ##[ ##1: #H5; napply (H2 y1 y2 H5); napply (triple_destruct_2 T1 T2 T3 … H4)
+ ##| ##2: #H5; napply (H3 z1 z2 H5); napply (triple_destruct_3 T1 T2 T3 … H4)
+ ##| ##3: #H5; napply (H1 x1 x2 H5); napply (triple_destruct_1 T1 T2 T3 … H4)
+ ##]
+nqed.
+
+nlemma triple_destruct
+ : ∀T1,T2,T3.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.(triple T1 T2 T3 x1 y1 z1) ≠ (triple T1 T2 T3 x2 y2 z2) →
+ Or3 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2).
+ #T1; #T2; #T3; #H1; #H2; #H3; #x1; #x2; #y1; #y2; #z1; #z2;
+ nnormalize; #H;
+ napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
+ ##[ ##1: #H4; napply (or3_intro1 … H4)
+ ##| ##2: #H4; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##1: #H5; napply (or3_intro2 … H5)
+ ##| ##2: #H5; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+ ##[ ##1: #H6; napply (or3_intro3 … H6)
+ ##| ##2: #H6; nrewrite > H4 in H:(%);
+ nrewrite > H5;
+ nrewrite > H6; #H; nelim (H (refl_eq …))
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqtriple :
+ ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ (∀x,y:T1.x ≠ y → f1 x y = false) →
+ (∀x,y:T2.x ≠ y → f2 x y = false) →
+ (∀x,y:T3.x ≠ y → f3 x y = false) →
+ (p1 ≠ p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = false).
+ #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6;
+ nelim p1;
+ #x1; #y1; #z1;
+ nelim p2;
+ #x2; #y2; #z2; #H;
+ nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2)) = false);
+ napply (or3_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) ? (triple_destruct T1 T2 T3 H1 H2 H3 … H) ?);
+ ##[ ##1: #H7; nrewrite > (H5 … H7); nrewrite > (andb_false3_2 (f1 x1 x2) (f3 z1 z2)); napply refl_eq
+ ##| ##2: #H7; nrewrite > (H6 … H7); nrewrite > (andb_false3_3 (f1 x1 x2) (f2 y1 y2)); napply refl_eq
+ ##| ##3: #H7; nrewrite > (H4 … H7); nrewrite > (andb_false3_1 (f2 y1 y2) (f3 z1 z2)); napply refl_eq
+ ##]
+nqed.
+
+(* ********* *)
+(* TUPLE x 4 *)
+(* ********* *)
+
nlemma quadruple_destruct_1 :
∀T1,T2,T3,T4.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
quadruple T1 T2 T3 T4 x1 y1 z1 v1 = quadruple T1 T2 T3 T4 x2 y2 z2 v2 → x1 = x2.
nlemma eq_to_eqquadruple :
∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
- (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
- (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
- (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
- (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
+ (∀x,y:T1.x = y → f1 x y = true) →
+ (∀x,y:T2.x = y → f2 x y = true) →
+ (∀x,y:T3.x = y → f3 x y = true) →
+ (∀x,y:T4.x = y → f4 x y = true) →
(p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
nelim p1;
nlemma eqquadruple_to_eq :
∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
- (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
- (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
- (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
- (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
+ (∀x,y:T1.f1 x y = true → x = y) →
+ (∀x,y:T2.f2 x y = true → x = y) →
+ (∀x,y:T3.f3 x y = true → x = y) →
+ (∀x,y:T4.f4 x y = true → x = y) →
(eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
#T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
nelim p1;
napply refl_eq.
nqed.
+nlemma decidable_quadruple
+ : ∀T1,T2,T3,T4.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ (∀x,y:T4.decidable (x = y)) →
+ ∀x,y:Prod4T T1 T2 T3 T4.decidable (x = y).
+ #T1; #T2; #T3; #T4; #H; #H1; #H2; #H3;
+ #x; nelim x; #xx1; #xx2; #xx3; #xx4;
+ #y; nelim y; #yy1; #yy2; #yy3; #yy4;
+ nnormalize;
+ napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
+ ##[ ##1: #H4; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H5; napply (H4 (quadruple_destruct_1 T1 T2 T3 T4 … H5))
+ ##| ##2: #H4; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+ ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H6; napply (H5 (quadruple_destruct_2 T1 T2 T3 T4 … H6))
+ ##| ##2: #H5; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+ ##[ ##1: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H7; napply (H6 (quadruple_destruct_3 T1 T2 T3 T4 … H7))
+ ##| ##2: #H6; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
+ ##[ ##1: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H8; napply (H7 (quadruple_destruct_4 T1 T2 T3 T4 … H8))
+ ##| ##2: #H7; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ nrewrite > H4;
+ nrewrite > H5;
+ nrewrite > H6;
+ nrewrite > H7;
+ napply refl_eq
+ ##]
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neqquadruple_to_neq :
+ ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (∀x,y:T1.f1 x y = false → x ≠ y) →
+ (∀x,y:T2.f2 x y = false → x ≠ y) →
+ (∀x,y:T3.f3 x y = false → x ≠ y) →
+ (∀x,y:T4.f4 x y = false → x ≠ y) →
+ (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2;
+ nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false) → ?); #H;
+ nnormalize; #H5;
+ napply (or4_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ? (andb_false4 … H) ?);
+ ##[ ##1: #H6; napply (H2 y1 y2 H6); napply (quadruple_destruct_2 T1 T2 T3 T4 … H5)
+ ##| ##2: #H6; napply (H3 z1 z2 H6); napply (quadruple_destruct_3 T1 T2 T3 T4 … H5)
+ ##| ##3: #H6; napply (H4 v1 v2 H6); napply (quadruple_destruct_4 T1 T2 T3 T4 … H5)
+ ##| ##4: #H6; napply (H1 x1 x2 H6); napply (quadruple_destruct_1 T1 T2 T3 T4 … H5)
+ ##]
+nqed.
+
+nlemma quadruple_destruct
+ : ∀T1,T2,T3,T4.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ (∀x,y:T4.decidable (x = y)) →
+ ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.
+ (quadruple T1 T2 T3 T4 x1 y1 z1 v1) ≠ (quadruple T1 T2 T3 T4 x2 y2 z2 v2) →
+ Or4 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2).
+ #T1; #T2; #T3; #T4; #H1; #H2; #H3; #H4;
+ #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2;
+ nnormalize; #H;
+ napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
+ ##[ ##1: #H5; napply (or4_intro1 … H5)
+ ##| ##2: #H5; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##1: #H6; napply (or4_intro2 … H6)
+ ##| ##2: #H6; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+ ##[ ##1: #H7; napply (or4_intro3 … H7)
+ ##| ##2: #H7; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
+ ##[ ##1: #H8; napply (or4_intro4 … H8)
+ ##| ##2: #H8; nrewrite > H5 in H:(%);
+ nrewrite > H6;
+ nrewrite > H7;
+ nrewrite > H8; #H; nelim (H (refl_eq …))
+ ##]
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqquadruple :
+ ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ (∀x,y:T4.decidable (x = y)) →
+ (∀x,y:T1.x ≠ y → f1 x y = false) →
+ (∀x,y:T2.x ≠ y → f2 x y = false) →
+ (∀x,y:T3.x ≠ y → f3 x y = false) →
+ (∀x,y:T4.x ≠ y → f4 x y = false) →
+ (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = false).
+ #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
+ nelim p1;
+ #x1; #y1; #z1; #v1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #H;
+ nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2)) = false);
+ napply (or4_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) ? (quadruple_destruct T1 T2 T3 T4 H1 H2 H3 H4 … H) ?);
+ ##[ ##1: #H9; nrewrite > (H6 … H9); nrewrite > (andb_false4_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##| ##2: #H9; nrewrite > (H7 … H9); nrewrite > (andb_false4_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2)); napply refl_eq
+ ##| ##3: #H9; nrewrite > (H8 … H9); nrewrite > (andb_false4_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2)); napply refl_eq
+ ##| ##4: #H9; nrewrite > (H5 … H9); nrewrite > (andb_false4_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##]
+nqed.
+
+(* ********* *)
+(* TUPLE x 5 *)
+(* ********* *)
+
nlemma quintuple_destruct_1 :
∀T1,T2,T3,T4,T5.∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1 = quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2 → x1 = x2.
nlemma eq_to_eqquintuple :
∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
- (∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
- (∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
- (∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
- (∀v1,v2:T4.v1 = v2 → f4 v1 v2 = true) →
- (∀w1,w2:T5.w1 = w2 → f5 w1 w2 = true) →
+ (∀x,y:T1.x = y → f1 x y = true) →
+ (∀x,y:T2.x = y → f2 x y = true) →
+ (∀x,y:T3.x = y → f3 x y = true) →
+ (∀x,y:T4.x = y → f4 x y = true) →
+ (∀x,y:T5.x = y → f5 x y = true) →
(p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
nelim p1;
nlemma eqquintuple_to_eq :
∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
- (∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
- (∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
- (∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
- (∀v1,v2:T4.f4 v1 v2 = true → v1 = v2) →
- (∀w1,w2:T5.f5 w1 w2 = true → w1 = w2) →
+ (∀x,y:T1.f1 x y = true → x = y) →
+ (∀x,y:T2.f2 x y = true → x = y) →
+ (∀x,y:T3.f3 x y = true → x = y) →
+ (∀x,y:T4.f4 x y = true → x = y) →
+ (∀x,y:T5.f5 x y = true → x = y) →
(eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
#T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
nelim p1;
nrewrite > (H5 w1 w2 H9);
napply refl_eq.
nqed.
+
+nlemma decidable_quintuple
+ : ∀T1,T2,T3,T4,T5.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ (∀x,y:T4.decidable (x = y)) →
+ (∀x,y:T5.decidable (x = y)) →
+ ∀x,y:Prod5T T1 T2 T3 T4 T5.decidable (x = y).
+ #T1; #T2; #T3; #T4; #T5; #H; #H1; #H2; #H3; #H4;
+ #x; nelim x; #xx1; #xx2; #xx3; #xx4; #xx5;
+ #y; nelim y; #yy1; #yy2; #yy3; #yy4; #yy5;
+ nnormalize;
+ napply (or2_elim (xx1 = yy1) (xx1 ≠ yy1) ? (H xx1 yy1) ?);
+ ##[ ##1: #H5; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H6; napply (H5 (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6))
+ ##| ##2: #H5; napply (or2_elim (xx2 = yy2) (xx2 ≠ yy2) ? (H1 xx2 yy2) ?);
+ ##[ ##1: #H6; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H7; napply (H6 (quintuple_destruct_2 T1 T2 T3 T4 T5 … H7))
+ ##| ##2: #H6; napply (or2_elim (xx3 = yy3) (xx3 ≠ yy3) ? (H2 xx3 yy3) ?);
+ ##[ ##1: #H7; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H8; napply (H7 (quintuple_destruct_3 T1 T2 T3 T4 T5 … H8))
+ ##| ##2: #H7; napply (or2_elim (xx4 = yy4) (xx4 ≠ yy4) ? (H3 xx4 yy4) ?);
+ ##[ ##1: #H8; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H9; napply (H8 (quintuple_destruct_4 T1 T2 T3 T4 T5 … H9))
+ ##| ##2: #H8; napply (or2_elim (xx5 = yy5) (xx5 ≠ yy5) ? (H4 xx5 yy5) ?);
+ ##[ ##1: #H9; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
+ nnormalize; #H10; napply (H9 (quintuple_destruct_5 T1 T2 T3 T4 T5 … H10))
+ ##| ##2: #H9; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
+ nrewrite > H5;
+ nrewrite > H6;
+ nrewrite > H7;
+ nrewrite > H8;
+ nrewrite > H9;
+ napply refl_eq
+ ##]
+ ##]
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neqquintuple_to_neq :
+ ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ (∀x,y:T1.f1 x y = false → x ≠ y) →
+ (∀x,y:T2.f2 x y = false → x ≠ y) →
+ (∀x,y:T3.f3 x y = false → x ≠ y) →
+ (∀x,y:T4.f4 x y = false → x ≠ y) →
+ (∀x,y:T5.f5 x y = false → x ≠ y) →
+ (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2;
+ nchange with ((((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false) → ?); #H;
+ nnormalize; #H6;
+ napply (or5_elim ((f1 x1 x2) = false) ((f2 y1 y2) = false) ((f3 z1 z2) = false) ((f4 v1 v2) = false) ((f5 w1 w2) = false) ? (andb_false5 … H) ?);
+ ##[ ##1: #H7; napply (H2 y1 y2 H7); napply (quintuple_destruct_2 T1 T2 T3 T4 T5 … H6)
+ ##| ##2: #H7; napply (H3 z1 z2 H7); napply (quintuple_destruct_3 T1 T2 T3 T4 T5 … H6)
+ ##| ##3: #H7; napply (H4 v1 v2 H7); napply (quintuple_destruct_4 T1 T2 T3 T4 T5 … H6)
+ ##| ##4: #H7; napply (H5 w1 w2 H7); napply (quintuple_destruct_5 T1 T2 T3 T4 T5 … H6)
+ ##| ##5: #H7; napply (H1 x1 x2 H7); napply (quintuple_destruct_1 T1 T2 T3 T4 T5 … H6)
+ ##]
+nqed.
+
+nlemma quintuple_destruct
+ : ∀T1,T2,T3,T4,T5.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ (∀x,y:T4.decidable (x = y)) →
+ (∀x,y:T5.decidable (x = y)) →
+ ∀x1,x2:T1.∀y1,y2:T2.∀z1,z2:T3.∀v1,v2:T4.∀w1,w2:T5.
+ (quintuple T1 T2 T3 T4 T5 x1 y1 z1 v1 w1) ≠ (quintuple T1 T2 T3 T4 T5 x2 y2 z2 v2 w2) →
+ Or5 (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2).
+ #T1; #T2; #T3; #T4; #T5; #H1; #H2; #H3; #H4; #H5;
+ #x1; #x2; #y1; #y2; #z1; #z2; #v1; #v2; #w1; #w2;
+ nnormalize; #H;
+ napply (or2_elim (x1 = x2) (x1 ≠ x2) ? (H1 x1 x2) ?);
+ ##[ ##1: #H6; napply (or5_intro1 … H6)
+ ##| ##2: #H6; napply (or2_elim (y1 = y2) (y1 ≠ y2) ? (H2 y1 y2) ?);
+ ##[ ##1: #H7; napply (or5_intro2 … H7)
+ ##| ##2: #H7; napply (or2_elim (z1 = z2) (z1 ≠ z2) ? (H3 z1 z2) ?);
+ ##[ ##1: #H8; napply (or5_intro3 … H8)
+ ##| ##2: #H8; napply (or2_elim (v1 = v2) (v1 ≠ v2) ? (H4 v1 v2) ?);
+ ##[ ##1: #H9; napply (or5_intro4 … H9)
+ ##| ##2: #H9; napply (or2_elim (w1 = w2) (w1 ≠ w2) ? (H5 w1 w2) ?);
+ ##[ ##1: #H10; napply (or5_intro5 … H10)
+ ##| ##2: #H10; nrewrite > H6 in H:(%);
+ nrewrite > H7;
+ nrewrite > H8;
+ nrewrite > H9;
+ nrewrite > H10; #H; nelim (H (refl_eq …))
+ ##]
+ ##]
+ ##]
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqquintuple :
+ ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+ ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+ (∀x,y:T1.decidable (x = y)) →
+ (∀x,y:T2.decidable (x = y)) →
+ (∀x,y:T3.decidable (x = y)) →
+ (∀x,y:T4.decidable (x = y)) →
+ (∀x,y:T5.decidable (x = y)) →
+ (∀x,y:T1.x ≠ y → f1 x y = false) →
+ (∀x,y:T2.x ≠ y → f2 x y = false) →
+ (∀x,y:T3.x ≠ y → f3 x y = false) →
+ (∀x,y:T4.x ≠ y → f4 x y = false) →
+ (∀x,y:T5.x ≠ y → f5 x y = false) →
+ (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = false).
+ #T1; #T2; #T3; #T4; #T5; #p1; #p2;
+ #f1; #f2; #f3; #f4; #f5;
+ #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10;
+ nelim p1;
+ #x1; #y1; #z1; #v1; #w1;
+ nelim p2;
+ #x2; #y2; #z2; #v2; #w2; #H;
+ nchange with (((f1 x1 x2) ⊗ (f2 y1 y2) ⊗ (f3 z1 z2) ⊗ (f4 v1 v2) ⊗ (f5 w1 w2)) = false);
+ napply (or5_elim (x1 ≠ x2) (y1 ≠ y2) (z1 ≠ z2) (v1 ≠ v2) (w1 ≠ w2) ? (quintuple_destruct T1 T2 T3 T4 T5 H1 H2 H3 H4 H5 … H) ?);
+ ##[ ##1: #H11; nrewrite > (H7 … H11); nrewrite > (andb_false5_2 (f1 x1 x2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##| ##2: #H11; nrewrite > (H8 … H11); nrewrite > (andb_false5_3 (f1 x1 x2) (f2 y1 y2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##| ##3: #H11; nrewrite > (H9 … H11); nrewrite > (andb_false5_4 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f5 w1 w2)); napply refl_eq
+ ##| ##4: #H11; nrewrite > (H10 … H11); nrewrite > (andb_false5_5 (f1 x1 x2) (f2 y1 y2) (f3 z1 z2) (f4 v1 v2)); napply refl_eq
+ ##| ##5: #H11; nrewrite > (H6 … H11); nrewrite > (andb_false5_1 (f2 y1 y2) (f3 z1 z2) (f4 v1 v2) (f5 w1 w2)); napply refl_eq
+ ##]
+nqed.
include "common/string.ma".
include "common/ascii_lemmas2.ma".
+include "common/ascii_lemmas3.ma".
+include "common/ascii_lemmas4.ma".
+include "common/ascii_lemmas5.ma".
include "common/list_utility_lemmas.ma".
(* ************************ *)
napply (eq_to_bfoldrightlist2 ascii eq_ascii s1 s2 eq_to_eqascii).
nqed.
+nlemma decidable_str : ∀x,y:list ascii.decidable (x = y).
+ napply (decidable_list ascii …);
+ napply decidable_ascii.
+nqed.
+
+nlemma neqstr_to_neq : ∀s,s'.eq_str s s' = false → s ≠ s'.
+ #s1; #s2;
+ napply (nbfoldrightlist2_to_neq ascii eq_ascii s1 s2 …);
+ napply neqascii_to_neq.
+nqed.
+
+nlemma neq_to_neqstr : ∀s,s'.s ≠ s' → eq_str s s' = false.
+ #s1; #s2;
+ napply (neq_to_nbfoldrightlist2 ascii eq_ascii s1 s2 …);
+ ##[ ##1: napply decidable_ascii
+ ##| ##2: napply neq_to_neqascii
+ ##]
+nqed.
+
(* ************ *)
(* STRINGA + ID *)
(* ************ *)
nnormalize;
napply refl_eq.
nqed.
+
+nlemma decidable_strid_aux1 : ∀s1,n1,s2,n2.s1 ≠ s2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
+ #s1; #n1; #s2; #n2;
+ nnormalize; #H; #H1;
+ napply (H (strid_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_strid_aux2 : ∀s1,n1,s2,n2.n1 ≠ n2 → (mk_strId s1 n1) ≠ (mk_strId s2 n2).
+ #s1; #n1; #s2; #n2;
+ nnormalize; #H; #H1;
+ napply (H (strid_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_strid : ∀x,y:strId.decidable (x = y).
+ #x; nelim x; #s1; #n1;
+ #y; nelim y; #s2; #n2;
+ nnormalize;
+ napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_strid_aux1 … H))
+ ##| ##1: #H; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_strid_aux2 … H1))
+ ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+ napply (or2_intro1 … (refl_eq ? (mk_strId s2 n2)))
+ ##]
+ ##]
+nqed.
+
+nlemma neqstrid_to_neq : ∀sid1,sid2:strId.(eq_strId sid1 sid2 = false) → (sid1 ≠ sid2).
+ #sid1; nelim sid1; #s1; #n1;
+ #sid2; nelim sid2; #s2; #n2;
+ nchange with ((((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false) → ?);
+ #H;
+ napply (or2_elim ((eq_str s1 s2) = false) ((eq_nat n1 n2) = false) ? (andb_false … H) …);
+ ##[ ##1: #H1; napply (decidable_strid_aux1 … (neqstr_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_strid_aux2 … (neqnat_to_neq … H1))
+ ##]
+nqed.
+
+nlemma strid_destruct : ∀s1,s2,n1,n2.(mk_strId s1 n1) ≠ (mk_strId s2 n2) → s1 ≠ s2 ∨ n1 ≠ n2.
+ #s1; #s2; #n1; #n2;
+ nnormalize; #H;
+ napply (or2_elim (s1 = s2) (s1 ≠ s2) ? (decidable_str s1 s2) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2) …);
+ ##[ ##2: #H2; napply (or2_intro2 … H2)
+ ##| ##1: #H2; nrewrite > H1 in H:(%);
+ nrewrite > H2;
+ #H; nelim (H (refl_eq …))
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqstrid : ∀sid1,sid2.sid1 ≠ sid2 → eq_strId sid1 sid2 = false.
+ #sid1; nelim sid1; #s1; #n1;
+ #sid2; nelim sid2; #s2; #n2;
+ #H; nchange with (((eq_str s1 s2) ⊗ (eq_nat n1 n2)) = false);
+ napply (or2_elim (s1 ≠ s2) (n1 ≠ n2) ? (strid_destruct … H) …);
+ ##[ ##1: #H1; nrewrite > (neq_to_neqstr … H1); nnormalize; napply refl_eq
+ ##| ##2: #H1; nrewrite > (neq_to_neqnat … H1);
+ nrewrite > (symmetric_andbool (eq_str s1 s2) false);
+ nnormalize; napply refl_eq
+ ##]
+nqed.
napply (H1 H).
nqed.
-ninductive And (A,B:Prop) : Prop ≝
- conj : A → B → (And A B).
+ninductive And2 (A,B:Prop) : Prop ≝
+ conj2 : A → B → (And2 A B).
-interpretation "logical and" 'and x y = (And x y).
+interpretation "logical and" 'and x y = (And2 x y).
-nlemma proj1: ∀A,B:Prop.A ∧ B → A.
+nlemma proj2_1: ∀A,B:Prop.A ∧ B → A.
#A; #B; #H;
- (* \ldots al posto di ??? *)
- napply (And_ind A B … H);
+ napply (And2_ind A B … H);
#H1; #H2;
napply H1.
nqed.
-nlemma proj2: ∀A,B:Prop.A ∧ B → B.
+nlemma proj2_2: ∀A,B:Prop.A ∧ B → B.
#A; #B; #H;
- napply (And_ind A B … H);
+ napply (And2_ind A B … H);
#H1; #H2;
napply H2.
nqed.
-ninductive Or (A,B:Prop) : Prop ≝
- or_introl : A → (Or A B)
-| or_intror : B → (Or A B).
+ninductive And3 (A,B,C:Prop) : Prop ≝
+ conj3 : A → B → C → (And3 A B C).
-interpretation "logical or" 'or x y = (Or x y).
+nlemma proj3_1: ∀A,B,C:Prop.And3 A B C → A.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H1.
+nqed.
+
+nlemma proj3_2: ∀A,B,C:Prop.And3 A B C → B.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H2.
+nqed.
+
+nlemma proj3_3: ∀A,B,C:Prop.And3 A B C → C.
+ #A; #B; #C; #H;
+ napply (And3_ind A B C … H);
+ #H1; #H2; #H3;
+ napply H3.
+nqed.
+
+ninductive And4 (A,B,C,D:Prop) : Prop ≝
+ conj4 : A → B → C → D → (And4 A B C D).
+
+nlemma proj4_1: ∀A,B,C,D:Prop.And4 A B C D → A.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H1.
+nqed.
+
+nlemma proj4_2: ∀A,B,C,D:Prop.And4 A B C D → B.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H2.
+nqed.
+
+nlemma proj4_3: ∀A,B,C,D:Prop.And4 A B C D → C.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H3.
+nqed.
+
+nlemma proj4_4: ∀A,B,C,D:Prop.And4 A B C D → D.
+ #A; #B; #C; #D; #H;
+ napply (And4_ind A B C D … H);
+ #H1; #H2; #H3; #H4;
+ napply H4.
+nqed.
+
+ninductive And5 (A,B,C,D,E:Prop) : Prop ≝
+ conj5 : A → B → C → D → E → (And5 A B C D E).
+
+nlemma proj5_1: ∀A,B,C,D,E:Prop.And5 A B C D E → A.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H1.
+nqed.
+
+nlemma proj5_2: ∀A,B,C,D,E:Prop.And5 A B C D E → B.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H2.
+nqed.
+
+nlemma proj5_3: ∀A,B,C,D,E:Prop.And5 A B C D E → C.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H3.
+nqed.
+
+nlemma proj5_4: ∀A,B,C,D,E:Prop.And5 A B C D E → D.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H4.
+nqed.
+
+nlemma proj5_5: ∀A,B,C,D,E:Prop.And5 A B C D E → E.
+ #A; #B; #C; #D; #E; #H;
+ napply (And5_ind A B C D E … H);
+ #H1; #H2; #H3; #H4; #H5;
+ napply H5.
+nqed.
+
+ninductive Or2 (A,B:Prop) : Prop ≝
+ or2_intro1 : A → (Or2 A B)
+| or2_intro2 : B → (Or2 A B).
+
+interpretation "logical or" 'or x y = (Or2 x y).
ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
-nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
- #P; #Q; #G; #H; #H1; #H2;
- napply (Or_ind P Q ? H1 H2 ?);
+nlemma or2_elim
+ : ∀P1,P2,Q:Prop.Or2 P1 P2 → ∀f1:P1 → Q.∀f2:P2 → Q.Q.
+ #P1; #P2; #Q; #H; #f1; #f2;
+ napply (Or2_ind P1 P2 ? f1 f2 ?);
+ napply H.
+nqed.
+
+ninductive Or3 (A,B,C:Prop) : Prop ≝
+ or3_intro1 : A → (Or3 A B C)
+| or3_intro2 : B → (Or3 A B C)
+| or3_intro3 : C → (Or3 A B C).
+
+nlemma or3_elim
+ : ∀P1,P2,P3,Q:Prop.Or3 P1 P2 P3 → ∀f1:P1 → Q.∀f2:P2 → Q.∀f3:P3 → Q.Q.
+ #P1; #P2; #P3; #Q; #H; #f1; #f2; #f3;
+ napply (Or3_ind P1 P2 P3 ? f1 f2 f3 ?);
+ napply H.
+nqed.
+
+ninductive Or4 (A,B,C,D:Prop) : Prop ≝
+ or4_intro1 : A → (Or4 A B C D)
+| or4_intro2 : B → (Or4 A B C D)
+| or4_intro3 : C → (Or4 A B C D)
+| or4_intro4 : D → (Or4 A B C D).
+
+nlemma or4_elim
+ : ∀P1,P2,P3,P4,Q:Prop.Or4 P1 P2 P3 P4 → ∀f1:P1 → Q.∀f2:P2 → Q.
+ ∀f3:P3 → Q.∀f4:P4 → Q.Q.
+ #P1; #P2; #P3; #P4; #Q; #H; #f1; #f2; #f3; #f4;
+ napply (Or4_ind P1 P2 P3 P4 ? f1 f2 f3 f4 ?);
+ napply H.
+nqed.
+
+ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
+ or5_intro1 : A → (Or5 A B C D E)
+| or5_intro2 : B → (Or5 A B C D E)
+| or5_intro3 : C → (Or5 A B C D E)
+| or5_intro4 : D → (Or5 A B C D E)
+| or5_intro5 : E → (Or5 A B C D E).
+
+nlemma or5_elim
+ : ∀P1,P2,P3,P4,P5,Q:Prop.Or5 P1 P2 P3 P4 P5 → ∀f1:P1 → Q.∀f2:P2 → Q.
+ ∀f3:P3 → Q.∀f4:P4 → Q.∀f5:P5 → Q.Q.
+ #P1; #P2; #P3; #P4; #P5; #Q; #H; #f1; #f2; #f3; #f4; #f5;
+ napply (Or5_ind P1 P2 P3 P4 P5 ? f1 f2 f3 f4 f5 ?);
napply H.
nqed.
common/nat.ma num/bool.ma
freescale/opcode_base_lemmas.ma freescale/opcode_base.ma num/bool_lemmas.ma
freescale_tests/medium_tests_tools.ma freescale/multivm.ma
-common/string_lemmas.ma common/ascii_lemmas2.ma common/list_utility_lemmas.ma common/string.ma
+common/string_lemmas.ma common/ascii_lemmas2.ma common/ascii_lemmas3.ma common/ascii_lemmas4.ma common/ascii_lemmas5.ma common/list_utility_lemmas.ma common/string.ma
compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma
num/quatern.ma num/bool.ma
freescale/table_HC05_tests.ma freescale/opcode.ma freescale/table_HC05.ma
ndefinition eq_bit ≝
λt1,t2:bitrigesim.
match t1 with
- [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ]
- | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
- | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ]
- | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
- | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ]
- | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
- | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ]
- | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
- | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ]
- | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
- | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ]
- | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
- | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ]
- | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
- | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ]
- | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
- | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ]
- | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
- | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ]
- | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
- | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ]
- | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
- | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ]
- | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
- | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ]
- | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
- | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ]
- | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
- | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ]
- | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
- | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ]
- | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
+ [ t00 ⇒ match t2 with [ t00 ⇒ true | _ ⇒ false ] | t01 ⇒ match t2 with [ t01 ⇒ true | _ ⇒ false ]
+ | t02 ⇒ match t2 with [ t02 ⇒ true | _ ⇒ false ] | t03 ⇒ match t2 with [ t03 ⇒ true | _ ⇒ false ]
+ | t04 ⇒ match t2 with [ t04 ⇒ true | _ ⇒ false ] | t05 ⇒ match t2 with [ t05 ⇒ true | _ ⇒ false ]
+ | t06 ⇒ match t2 with [ t06 ⇒ true | _ ⇒ false ] | t07 ⇒ match t2 with [ t07 ⇒ true | _ ⇒ false ]
+ | t08 ⇒ match t2 with [ t08 ⇒ true | _ ⇒ false ] | t09 ⇒ match t2 with [ t09 ⇒ true | _ ⇒ false ]
+ | t0A ⇒ match t2 with [ t0A ⇒ true | _ ⇒ false ] | t0B ⇒ match t2 with [ t0B ⇒ true | _ ⇒ false ]
+ | t0C ⇒ match t2 with [ t0C ⇒ true | _ ⇒ false ] | t0D ⇒ match t2 with [ t0D ⇒ true | _ ⇒ false ]
+ | t0E ⇒ match t2 with [ t0E ⇒ true | _ ⇒ false ] | t0F ⇒ match t2 with [ t0F ⇒ true | _ ⇒ false ]
+ | t10 ⇒ match t2 with [ t10 ⇒ true | _ ⇒ false ] | t11 ⇒ match t2 with [ t11 ⇒ true | _ ⇒ false ]
+ | t12 ⇒ match t2 with [ t12 ⇒ true | _ ⇒ false ] | t13 ⇒ match t2 with [ t13 ⇒ true | _ ⇒ false ]
+ | t14 ⇒ match t2 with [ t14 ⇒ true | _ ⇒ false ] | t15 ⇒ match t2 with [ t15 ⇒ true | _ ⇒ false ]
+ | t16 ⇒ match t2 with [ t16 ⇒ true | _ ⇒ false ] | t17 ⇒ match t2 with [ t17 ⇒ true | _ ⇒ false ]
+ | t18 ⇒ match t2 with [ t18 ⇒ true | _ ⇒ false ] | t19 ⇒ match t2 with [ t19 ⇒ true | _ ⇒ false ]
+ | t1A ⇒ match t2 with [ t1A ⇒ true | _ ⇒ false ] | t1B ⇒ match t2 with [ t1B ⇒ true | _ ⇒ false ]
+ | t1C ⇒ match t2 with [ t1C ⇒ true | _ ⇒ false ] | t1D ⇒ match t2 with [ t1D ⇒ true | _ ⇒ false ]
+ | t1E ⇒ match t2 with [ t1E ⇒ true | _ ⇒ false ] | t1F ⇒ match t2 with [ t1F ⇒ true | _ ⇒ false ]
].
(* iteratore sui bitrigesimali *)
ndefinition bitrigesim_destruct_aux ≝
Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
match t1 with
- [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
- | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
- | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
- | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
- | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
- | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
- | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
- | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
- | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
- | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
- | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
- | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
- | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
- | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
- | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
- | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
- | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
- | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
- | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
- | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
- | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
- | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
- | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
- | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
- | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
- | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
- | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
- | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
- | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
- | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
- | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
- | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
+ [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ] | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
+ | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ] | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
+ | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ] | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
+ | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ] | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
+ | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ] | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
+ | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ] | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
+ | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ] | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
+ | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ] | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
+ | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ] | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
+ | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ] | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
+ | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ] | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
+ | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ] | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
+ | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ] | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
+ | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ] | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
+ | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ] | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
+ | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ] | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
].
ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
#t1;
ncases t1;
- ##[ ##1: napply bitrigesim_destruct1
- ##| ##2: napply bitrigesim_destruct2
- ##| ##3: napply bitrigesim_destruct3
- ##| ##4: napply bitrigesim_destruct4
- ##| ##5: napply bitrigesim_destruct5
- ##| ##6: napply bitrigesim_destruct6
- ##| ##7: napply bitrigesim_destruct7
- ##| ##8: napply bitrigesim_destruct8
- ##| ##9: napply bitrigesim_destruct9
- ##| ##10: napply bitrigesim_destruct10
- ##| ##11: napply bitrigesim_destruct11
- ##| ##12: napply bitrigesim_destruct12
- ##| ##13: napply bitrigesim_destruct13
- ##| ##14: napply bitrigesim_destruct14
- ##| ##15: napply bitrigesim_destruct15
- ##| ##16: napply bitrigesim_destruct16
- ##| ##17: napply bitrigesim_destruct17
- ##| ##18: napply bitrigesim_destruct18
- ##| ##19: napply bitrigesim_destruct19
- ##| ##20: napply bitrigesim_destruct20
- ##| ##21: napply bitrigesim_destruct21
- ##| ##22: napply bitrigesim_destruct22
- ##| ##23: napply bitrigesim_destruct23
- ##| ##24: napply bitrigesim_destruct24
- ##| ##25: napply bitrigesim_destruct25
- ##| ##26: napply bitrigesim_destruct26
- ##| ##27: napply bitrigesim_destruct27
- ##| ##28: napply bitrigesim_destruct28
- ##| ##29: napply bitrigesim_destruct29
- ##| ##30: napply bitrigesim_destruct30
- ##| ##31: napply bitrigesim_destruct31
- ##| ##32: napply bitrigesim_destruct32
+ ##[ ##1: napply bitrigesim_destruct1 ##| ##2: napply bitrigesim_destruct2
+ ##| ##3: napply bitrigesim_destruct3 ##| ##4: napply bitrigesim_destruct4
+ ##| ##5: napply bitrigesim_destruct5 ##| ##6: napply bitrigesim_destruct6
+ ##| ##7: napply bitrigesim_destruct7 ##| ##8: napply bitrigesim_destruct8
+ ##| ##9: napply bitrigesim_destruct9 ##| ##10: napply bitrigesim_destruct10
+ ##| ##11: napply bitrigesim_destruct11 ##| ##12: napply bitrigesim_destruct12
+ ##| ##13: napply bitrigesim_destruct13 ##| ##14: napply bitrigesim_destruct14
+ ##| ##15: napply bitrigesim_destruct15 ##| ##16: napply bitrigesim_destruct16
+ ##| ##17: napply bitrigesim_destruct17 ##| ##18: napply bitrigesim_destruct18
+ ##| ##19: napply bitrigesim_destruct19 ##| ##20: napply bitrigesim_destruct20
+ ##| ##21: napply bitrigesim_destruct21 ##| ##22: napply bitrigesim_destruct22
+ ##| ##23: napply bitrigesim_destruct23 ##| ##24: napply bitrigesim_destruct24
+ ##| ##25: napply bitrigesim_destruct25 ##| ##26: napply bitrigesim_destruct26
+ ##| ##27: napply bitrigesim_destruct27 ##| ##28: napply bitrigesim_destruct28
+ ##| ##29: napply bitrigesim_destruct29 ##| ##30: napply bitrigesim_destruct30
+ ##| ##31: napply bitrigesim_destruct31 ##| ##32: napply bitrigesim_destruct32
##]
nqed.
nqed.
nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
- #t1;
- ncases t1;
- ##[ ##1: napply eqbit_to_eq1
- ##| ##2: napply eqbit_to_eq2
- ##| ##3: napply eqbit_to_eq3
- ##| ##4: napply eqbit_to_eq4
- ##| ##5: napply eqbit_to_eq5
- ##| ##6: napply eqbit_to_eq6
- ##| ##7: napply eqbit_to_eq7
- ##| ##8: napply eqbit_to_eq8
- ##| ##9: napply eqbit_to_eq9
- ##| ##10: napply eqbit_to_eq10
- ##| ##11: napply eqbit_to_eq11
- ##| ##12: napply eqbit_to_eq12
- ##| ##13: napply eqbit_to_eq13
- ##| ##14: napply eqbit_to_eq14
- ##| ##15: napply eqbit_to_eq15
- ##| ##16: napply eqbit_to_eq16
- ##| ##17: napply eqbit_to_eq17
- ##| ##18: napply eqbit_to_eq18
- ##| ##19: napply eqbit_to_eq19
- ##| ##20: napply eqbit_to_eq20
- ##| ##21: napply eqbit_to_eq21
- ##| ##22: napply eqbit_to_eq22
- ##| ##23: napply eqbit_to_eq23
- ##| ##24: napply eqbit_to_eq24
- ##| ##25: napply eqbit_to_eq25
- ##| ##26: napply eqbit_to_eq26
- ##| ##27: napply eqbit_to_eq27
- ##| ##28: napply eqbit_to_eq28
- ##| ##29: napply eqbit_to_eq29
- ##| ##30: napply eqbit_to_eq30
- ##| ##31: napply eqbit_to_eq31
- ##| ##32: napply eqbit_to_eq32
+ #t1; ncases t1;
+ ##[ ##1: napply eqbit_to_eq1 ##| ##2: napply eqbit_to_eq2
+ ##| ##3: napply eqbit_to_eq3 ##| ##4: napply eqbit_to_eq4
+ ##| ##5: napply eqbit_to_eq5 ##| ##6: napply eqbit_to_eq6
+ ##| ##7: napply eqbit_to_eq7 ##| ##8: napply eqbit_to_eq8
+ ##| ##9: napply eqbit_to_eq9 ##| ##10: napply eqbit_to_eq10
+ ##| ##11: napply eqbit_to_eq11 ##| ##12: napply eqbit_to_eq12
+ ##| ##13: napply eqbit_to_eq13 ##| ##14: napply eqbit_to_eq14
+ ##| ##15: napply eqbit_to_eq15 ##| ##16: napply eqbit_to_eq16
+ ##| ##17: napply eqbit_to_eq17 ##| ##18: napply eqbit_to_eq18
+ ##| ##19: napply eqbit_to_eq19 ##| ##20: napply eqbit_to_eq20
+ ##| ##21: napply eqbit_to_eq21 ##| ##22: napply eqbit_to_eq22
+ ##| ##23: napply eqbit_to_eq23 ##| ##24: napply eqbit_to_eq24
+ ##| ##25: napply eqbit_to_eq25 ##| ##26: napply eqbit_to_eq26
+ ##| ##27: napply eqbit_to_eq27 ##| ##28: napply eqbit_to_eq28
+ ##| ##29: napply eqbit_to_eq29 ##| ##30: napply eqbit_to_eq30
+ ##| ##31: napply eqbit_to_eq31 ##| ##32: napply eqbit_to_eq32
##]
nqed.
nqed.
nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
- #t1;
- ncases t1;
- ##[ ##1: napply eq_to_eqbit1
- ##| ##2: napply eq_to_eqbit2
- ##| ##3: napply eq_to_eqbit3
- ##| ##4: napply eq_to_eqbit4
- ##| ##5: napply eq_to_eqbit5
- ##| ##6: napply eq_to_eqbit6
- ##| ##7: napply eq_to_eqbit7
- ##| ##8: napply eq_to_eqbit8
- ##| ##9: napply eq_to_eqbit9
- ##| ##10: napply eq_to_eqbit10
- ##| ##11: napply eq_to_eqbit11
- ##| ##12: napply eq_to_eqbit12
- ##| ##13: napply eq_to_eqbit13
- ##| ##14: napply eq_to_eqbit14
- ##| ##15: napply eq_to_eqbit15
- ##| ##16: napply eq_to_eqbit16
- ##| ##17: napply eq_to_eqbit17
- ##| ##18: napply eq_to_eqbit18
- ##| ##19: napply eq_to_eqbit19
- ##| ##20: napply eq_to_eqbit20
- ##| ##21: napply eq_to_eqbit21
- ##| ##22: napply eq_to_eqbit22
- ##| ##23: napply eq_to_eqbit23
- ##| ##24: napply eq_to_eqbit24
- ##| ##25: napply eq_to_eqbit25
- ##| ##26: napply eq_to_eqbit26
- ##| ##27: napply eq_to_eqbit27
- ##| ##28: napply eq_to_eqbit28
- ##| ##29: napply eq_to_eqbit29
- ##| ##30: napply eq_to_eqbit30
- ##| ##31: napply eq_to_eqbit31
- ##| ##32: napply eq_to_eqbit32
+ #t1; ncases t1;
+ ##[ ##1: napply eq_to_eqbit1 ##| ##2: napply eq_to_eqbit2
+ ##| ##3: napply eq_to_eqbit3 ##| ##4: napply eq_to_eqbit4
+ ##| ##5: napply eq_to_eqbit5 ##| ##6: napply eq_to_eqbit6
+ ##| ##7: napply eq_to_eqbit7 ##| ##8: napply eq_to_eqbit8
+ ##| ##9: napply eq_to_eqbit9 ##| ##10: napply eq_to_eqbit10
+ ##| ##11: napply eq_to_eqbit11 ##| ##12: napply eq_to_eqbit12
+ ##| ##13: napply eq_to_eqbit13 ##| ##14: napply eq_to_eqbit14
+ ##| ##15: napply eq_to_eqbit15 ##| ##16: napply eq_to_eqbit16
+ ##| ##17: napply eq_to_eqbit17 ##| ##18: napply eq_to_eqbit18
+ ##| ##19: napply eq_to_eqbit19 ##| ##20: napply eq_to_eqbit20
+ ##| ##21: napply eq_to_eqbit21 ##| ##22: napply eq_to_eqbit22
+ ##| ##23: napply eq_to_eqbit23 ##| ##24: napply eq_to_eqbit24
+ ##| ##25: napply eq_to_eqbit25 ##| ##26: napply eq_to_eqbit26
+ ##| ##27: napply eq_to_eqbit27 ##| ##28: napply eq_to_eqbit28
+ ##| ##29: napply eq_to_eqbit29 ##| ##30: napply eq_to_eqbit30
+ ##| ##31: napply eq_to_eqbit31 ##| ##32: napply eq_to_eqbit32
##]
nqed.
nlemma decidable_bit1 : ∀x:bitrigesim.decidable (t00 = x).
#x; nnormalize; nelim x;
- ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit2 : ∀x:bitrigesim.decidable (t01 = x).
#x; nnormalize; nelim x;
- ##[ ##2: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit3 : ∀x:bitrigesim.decidable (t02 = x).
#x; nnormalize; nelim x;
- ##[ ##3: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit4 : ∀x:bitrigesim.decidable (t03 = x).
#x; nnormalize; nelim x;
- ##[ ##4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit5 : ∀x:bitrigesim.decidable (t04 = x).
#x; nnormalize; nelim x;
- ##[ ##5: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit6 : ∀x:bitrigesim.decidable (t05 = x).
#x; nnormalize; nelim x;
- ##[ ##6: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit7 : ∀x:bitrigesim.decidable (t06 = x).
#x; nnormalize; nelim x;
- ##[ ##7: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit8 : ∀x:bitrigesim.decidable (t07 = x).
#x; nnormalize; nelim x;
- ##[ ##8: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit9 : ∀x:bitrigesim.decidable (t08 = x).
#x; nnormalize; nelim x;
- ##[ ##9: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit10 : ∀x:bitrigesim.decidable (t09 = x).
#x; nnormalize; nelim x;
- ##[ ##10: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit11 : ∀x:bitrigesim.decidable (t0A = x).
#x; nnormalize; nelim x;
- ##[ ##11: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit12 : ∀x:bitrigesim.decidable (t0B = x).
#x; nnormalize; nelim x;
- ##[ ##12: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit13 : ∀x:bitrigesim.decidable (t0C = x).
#x; nnormalize; nelim x;
- ##[ ##13: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit14 : ∀x:bitrigesim.decidable (t0D = x).
#x; nnormalize; nelim x;
- ##[ ##14: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit15 : ∀x:bitrigesim.decidable (t0E = x).
#x; nnormalize; nelim x;
- ##[ ##15: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit16 : ∀x:bitrigesim.decidable (t0F = x).
#x; nnormalize; nelim x;
- ##[ ##16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit17 : ∀x:bitrigesim.decidable (t10 = x).
#x; nnormalize; nelim x;
- ##[ ##17: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit18 : ∀x:bitrigesim.decidable (t11 = x).
#x; nnormalize; nelim x;
- ##[ ##18: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit19 : ∀x:bitrigesim.decidable (t12 = x).
#x; nnormalize; nelim x;
- ##[ ##19: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit20 : ∀x:bitrigesim.decidable (t13 = x).
#x; nnormalize; nelim x;
- ##[ ##20: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit21 : ∀x:bitrigesim.decidable (t14 = x).
#x; nnormalize; nelim x;
- ##[ ##21: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit22 : ∀x:bitrigesim.decidable (t15 = x).
#x; nnormalize; nelim x;
- ##[ ##22: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit23 : ∀x:bitrigesim.decidable (t16 = x).
#x; nnormalize; nelim x;
- ##[ ##23: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit24 : ∀x:bitrigesim.decidable (t17 = x).
#x; nnormalize; nelim x;
- ##[ ##24: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit25 : ∀x:bitrigesim.decidable (t18 = x).
#x; nnormalize; nelim x;
- ##[ ##25: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit26 : ∀x:bitrigesim.decidable (t19 = x).
#x; nnormalize; nelim x;
- ##[ ##26: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit27 : ∀x:bitrigesim.decidable (t1A = x).
#x; nnormalize; nelim x;
- ##[ ##27: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit28 : ∀x:bitrigesim.decidable (t1B = x).
#x; nnormalize; nelim x;
- ##[ ##28: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit29 : ∀x:bitrigesim.decidable (t1C = x).
#x; nnormalize; nelim x;
- ##[ ##29: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit30 : ∀x:bitrigesim.decidable (t1D = x).
#x; nnormalize; nelim x;
- ##[ ##30: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit31 : ∀x:bitrigesim.decidable (t1E = x).
#x; nnormalize; nelim x;
- ##[ ##31: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit32 : ∀x:bitrigesim.decidable (t1F = x).
#x; nnormalize; nelim x;
- ##[ ##32: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
##]
nqed.
nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
#x; nnormalize; nelim x;
- ##[ ##1: napply decidable_bit1
- ##| ##2: napply decidable_bit2
- ##| ##3: napply decidable_bit3
- ##| ##4: napply decidable_bit4
- ##| ##5: napply decidable_bit5
- ##| ##6: napply decidable_bit6
- ##| ##7: napply decidable_bit7
- ##| ##8: napply decidable_bit8
- ##| ##9: napply decidable_bit9
- ##| ##10: napply decidable_bit10
- ##| ##11: napply decidable_bit11
- ##| ##12: napply decidable_bit12
- ##| ##13: napply decidable_bit13
- ##| ##14: napply decidable_bit14
- ##| ##15: napply decidable_bit15
- ##| ##16: napply decidable_bit16
- ##| ##17: napply decidable_bit17
- ##| ##18: napply decidable_bit18
- ##| ##19: napply decidable_bit19
- ##| ##20: napply decidable_bit20
- ##| ##21: napply decidable_bit21
- ##| ##22: napply decidable_bit22
- ##| ##23: napply decidable_bit23
- ##| ##24: napply decidable_bit24
- ##| ##25: napply decidable_bit25
- ##| ##26: napply decidable_bit26
- ##| ##27: napply decidable_bit27
- ##| ##28: napply decidable_bit28
- ##| ##29: napply decidable_bit29
- ##| ##30: napply decidable_bit30
- ##| ##31: napply decidable_bit31
- ##| ##32: napply decidable_bit32
+ ##[ ##1: napply decidable_bit1 ##| ##2: napply decidable_bit2
+ ##| ##3: napply decidable_bit3 ##| ##4: napply decidable_bit4
+ ##| ##5: napply decidable_bit5 ##| ##6: napply decidable_bit6
+ ##| ##7: napply decidable_bit7 ##| ##8: napply decidable_bit8
+ ##| ##9: napply decidable_bit9 ##| ##10: napply decidable_bit10
+ ##| ##11: napply decidable_bit11 ##| ##12: napply decidable_bit12
+ ##| ##13: napply decidable_bit13 ##| ##14: napply decidable_bit14
+ ##| ##15: napply decidable_bit15 ##| ##16: napply decidable_bit16
+ ##| ##17: napply decidable_bit17 ##| ##18: napply decidable_bit18
+ ##| ##19: napply decidable_bit19 ##| ##20: napply decidable_bit20
+ ##| ##21: napply decidable_bit21 ##| ##22: napply decidable_bit22
+ ##| ##23: napply decidable_bit23 ##| ##24: napply decidable_bit24
+ ##| ##25: napply decidable_bit25 ##| ##26: napply decidable_bit26
+ ##| ##27: napply decidable_bit27 ##| ##28: napply decidable_bit28
+ ##| ##29: napply decidable_bit29 ##| ##30: napply decidable_bit30
+ ##| ##31: napply decidable_bit31 ##| ##32: napply decidable_bit32
##]
nqed.
nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2.
#t1; nelim t1;
- ##[ ##1: napply neqbit_to_neq1
- ##| ##2: napply neqbit_to_neq2
- ##| ##3: napply neqbit_to_neq3
- ##| ##4: napply neqbit_to_neq4
- ##| ##5: napply neqbit_to_neq5
- ##| ##6: napply neqbit_to_neq6
- ##| ##7: napply neqbit_to_neq7
- ##| ##8: napply neqbit_to_neq8
- ##| ##9: napply neqbit_to_neq9
- ##| ##10: napply neqbit_to_neq10
- ##| ##11: napply neqbit_to_neq11
- ##| ##12: napply neqbit_to_neq12
- ##| ##13: napply neqbit_to_neq13
- ##| ##14: napply neqbit_to_neq14
- ##| ##15: napply neqbit_to_neq15
- ##| ##16: napply neqbit_to_neq16
- ##| ##17: napply neqbit_to_neq17
- ##| ##18: napply neqbit_to_neq18
- ##| ##19: napply neqbit_to_neq19
- ##| ##20: napply neqbit_to_neq20
- ##| ##21: napply neqbit_to_neq21
- ##| ##22: napply neqbit_to_neq22
- ##| ##23: napply neqbit_to_neq23
- ##| ##24: napply neqbit_to_neq24
- ##| ##25: napply neqbit_to_neq25
- ##| ##26: napply neqbit_to_neq26
- ##| ##27: napply neqbit_to_neq27
- ##| ##28: napply neqbit_to_neq28
- ##| ##29: napply neqbit_to_neq29
- ##| ##30: napply neqbit_to_neq30
- ##| ##31: napply neqbit_to_neq31
- ##| ##32: napply neqbit_to_neq32
+ ##[ ##1: napply neqbit_to_neq1 ##| ##2: napply neqbit_to_neq2
+ ##| ##3: napply neqbit_to_neq3 ##| ##4: napply neqbit_to_neq4
+ ##| ##5: napply neqbit_to_neq5 ##| ##6: napply neqbit_to_neq6
+ ##| ##7: napply neqbit_to_neq7 ##| ##8: napply neqbit_to_neq8
+ ##| ##9: napply neqbit_to_neq9 ##| ##10: napply neqbit_to_neq10
+ ##| ##11: napply neqbit_to_neq11 ##| ##12: napply neqbit_to_neq12
+ ##| ##13: napply neqbit_to_neq13 ##| ##14: napply neqbit_to_neq14
+ ##| ##15: napply neqbit_to_neq15 ##| ##16: napply neqbit_to_neq16
+ ##| ##17: napply neqbit_to_neq17 ##| ##18: napply neqbit_to_neq18
+ ##| ##19: napply neqbit_to_neq19 ##| ##20: napply neqbit_to_neq20
+ ##| ##21: napply neqbit_to_neq21 ##| ##22: napply neqbit_to_neq22
+ ##| ##23: napply neqbit_to_neq23 ##| ##24: napply neqbit_to_neq24
+ ##| ##25: napply neqbit_to_neq25 ##| ##26: napply neqbit_to_neq26
+ ##| ##27: napply neqbit_to_neq27 ##| ##28: napply neqbit_to_neq28
+ ##| ##29: napply neqbit_to_neq29 ##| ##30: napply neqbit_to_neq30
+ ##| ##31: napply neqbit_to_neq31 ##| ##32: napply neqbit_to_neq32
##]
nqed.
nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false.
#t1; nelim t1;
- ##[ ##1: napply neq_to_neqbit1
- ##| ##2: napply neq_to_neqbit2
- ##| ##3: napply neq_to_neqbit3
- ##| ##4: napply neq_to_neqbit4
- ##| ##5: napply neq_to_neqbit5
- ##| ##6: napply neq_to_neqbit6
- ##| ##7: napply neq_to_neqbit7
- ##| ##8: napply neq_to_neqbit8
- ##| ##9: napply neq_to_neqbit9
- ##| ##10: napply neq_to_neqbit10
- ##| ##11: napply neq_to_neqbit11
- ##| ##12: napply neq_to_neqbit12
- ##| ##13: napply neq_to_neqbit13
- ##| ##14: napply neq_to_neqbit14
- ##| ##15: napply neq_to_neqbit15
- ##| ##16: napply neq_to_neqbit16
- ##| ##17: napply neq_to_neqbit17
- ##| ##18: napply neq_to_neqbit18
- ##| ##19: napply neq_to_neqbit19
- ##| ##20: napply neq_to_neqbit20
- ##| ##21: napply neq_to_neqbit21
- ##| ##22: napply neq_to_neqbit22
- ##| ##23: napply neq_to_neqbit23
- ##| ##24: napply neq_to_neqbit24
- ##| ##25: napply neq_to_neqbit25
- ##| ##26: napply neq_to_neqbit26
- ##| ##27: napply neq_to_neqbit27
- ##| ##28: napply neq_to_neqbit28
- ##| ##29: napply neq_to_neqbit29
- ##| ##30: napply neq_to_neqbit30
- ##| ##31: napply neq_to_neqbit31
- ##| ##32: napply neq_to_neqbit32
+ ##[ ##1: napply neq_to_neqbit1 ##| ##2: napply neq_to_neqbit2
+ ##| ##3: napply neq_to_neqbit3 ##| ##4: napply neq_to_neqbit4
+ ##| ##5: napply neq_to_neqbit5 ##| ##6: napply neq_to_neqbit6
+ ##| ##7: napply neq_to_neqbit7 ##| ##8: napply neq_to_neqbit8
+ ##| ##9: napply neq_to_neqbit9 ##| ##10: napply neq_to_neqbit10
+ ##| ##11: napply neq_to_neqbit11 ##| ##12: napply neq_to_neqbit12
+ ##| ##13: napply neq_to_neqbit13 ##| ##14: napply neq_to_neqbit14
+ ##| ##15: napply neq_to_neqbit15 ##| ##16: napply neq_to_neqbit16
+ ##| ##17: napply neq_to_neqbit17 ##| ##18: napply neq_to_neqbit18
+ ##| ##19: napply neq_to_neqbit19 ##| ##20: napply neq_to_neqbit20
+ ##| ##21: napply neq_to_neqbit21 ##| ##22: napply neq_to_neqbit22
+ ##| ##23: napply neq_to_neqbit23 ##| ##24: napply neq_to_neqbit24
+ ##| ##25: napply neq_to_neqbit25 ##| ##26: napply neq_to_neqbit26
+ ##| ##27: napply neq_to_neqbit27 ##| ##28: napply neq_to_neqbit28
+ ##| ##29: napply neq_to_neqbit29 ##| ##30: napply neq_to_neqbit30
+ ##| ##31: napply neq_to_neqbit31 ##| ##32: napply neq_to_neqbit32
##]
nqed.
nnormalize;
nelim x;
nelim y;
- ##[ ##1,4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bool_destruct … H)
+ ##[ ##1,4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bool_destruct … H)
##]
nqed.
##]
nqed.
-nlemma andb_false : ∀b1,b2.(b1 ⊗ b2) = false → (b1 = false) ∨ (b2 = false).
+nlemma andb_false2
+ : ∀b1,b2.(b1 ⊗ b2) = false →
+ (b1 = false) ∨ (b2 = false).
#b1; #b2;
ncases b1;
ncases b2;
nnormalize;
##[ ##1: #H; napply (bool_destruct … H)
- ##| ##2,4: #H; napply (or_intror … H)
- ##| ##3: #H; napply (or_introl … H)
+ ##| ##2,4: #H; napply (or2_intro2 … H)
+ ##| ##3: #H; napply (or2_intro1 … H)
##]
nqed.
+nlemma andb_false3
+ : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ b3) = false →
+ Or3 (b1 = false) (b2 = false) (b3 = false).
+ #b1; #b2; #b3;
+ ncases b1;
+ ncases b2;
+ ncases b3;
+ nnormalize;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##5,6,7,8: #H; napply (or3_intro1 … H)
+ ##| ##2,4: #H; napply (or3_intro3 … H)
+ ##| ##3: #H; napply (or3_intro2 … H)
+ ##]
+nqed.
+
+nlemma andb_false4
+ : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ b4) = false →
+ Or4 (b1 = false) (b2 = false) (b3 = false) (b4 = false).
+ #b1; #b2; #b3; #b4;
+ ncases b1;
+ ncases b2;
+ ncases b3;
+ ncases b4;
+ nnormalize;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##9,10,11,12,13,14,15,16: #H; napply (or4_intro1 … H)
+ ##| ##5,6,7,8: #H; napply (or4_intro2 … H)
+ ##| ##3,4: #H; napply (or4_intro3 … H)
+ ##| ##2: #H; napply (or4_intro4 … H)
+ ##]
+nqed.
+
+nlemma andb_false5
+ : ∀b1,b2,b3,b4,b5.(b1 ⊗ b2 ⊗ b3 ⊗ b4 ⊗ b5) = false →
+ Or5 (b1 = false) (b2 = false) (b3 = false) (b4 = false) (b5 = false).
+ #b1; #b2; #b3; #b4; #b5;
+ ncases b1;
+ ncases b2;
+ ncases b3;
+ ncases b4;
+ ncases b5;
+ nnormalize;
+ ##[ ##1: #H; napply (bool_destruct … H)
+ ##| ##17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #H; napply (or5_intro1 … H)
+ ##| ##9,10,11,12,13,14,15,16: #H; napply (or5_intro2 … H)
+ ##| ##5,6,7,8: #H; napply (or5_intro3 … H)
+ ##| ##3,4: #H; napply (or5_intro4 … H)
+ ##| ##2: #H; napply (or5_intro5 … H)
+ ##]
+nqed.
+
+nlemma andb_false2_1 : ∀b.(false ⊗ b) = false.
+ #b; nnormalize; napply refl_eq. nqed.
+nlemma andb_false2_2 : ∀b.(b ⊗ false) = false.
+ #b; nelim b; nnormalize; napply refl_eq. nqed.
+
+nlemma andb_false3_1 : ∀b1,b2.(false ⊗ b1 ⊗ b2) = false.
+ #b1; #b2; nnormalize; napply refl_eq. nqed.
+nlemma andb_false3_2 : ∀b1,b2.(b1 ⊗ false ⊗ b2) = false.
+ #b1; #b2; nelim b1; nnormalize; napply refl_eq. nqed.
+nlemma andb_false3_3 : ∀b1,b2.(b1 ⊗ b2 ⊗ false) = false.
+ #b1; #b2; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed.
+
+nlemma andb_false4_1 : ∀b1,b2,b3.(false ⊗ b1 ⊗ b2 ⊗ b3) = false.
+ #b1; #b2; #b3; nnormalize; napply refl_eq. nqed.
+nlemma andb_false4_2 : ∀b1,b2,b3.(b1 ⊗ false ⊗ b2 ⊗ b3) = false.
+ #b1; #b2; #b3; nelim b1; nnormalize; napply refl_eq. nqed.
+nlemma andb_false4_3 : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ false ⊗ b3) = false.
+ #b1; #b2; #b3; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed.
+nlemma andb_false4_4 : ∀b1,b2,b3.(b1 ⊗ b2 ⊗ b3 ⊗ false) = false.
+ #b1; #b2; #b3; nelim b1; nelim b2; nelim b3; nnormalize; napply refl_eq. nqed.
+
+nlemma andb_false5_1 : ∀b1,b2,b3,b4.(false ⊗ b1 ⊗ b2 ⊗ b3 ⊗ b4) = false.
+ #b1; #b2; #b3; #b4; nnormalize; napply refl_eq. nqed.
+nlemma andb_false5_2 : ∀b1,b2,b3,b4.(b1 ⊗ false ⊗ b2 ⊗ b3 ⊗ b4) = false.
+ #b1; #b2; #b3; #b4; nelim b1; nnormalize; napply refl_eq. nqed.
+nlemma andb_false5_3 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ false ⊗ b3 ⊗ b4) = false.
+ #b1; #b2; #b3; #b4; nelim b1; nelim b2; nnormalize; napply refl_eq. nqed.
+nlemma andb_false5_4 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ false ⊗ b4) = false.
+ #b1; #b2; #b3; #b4; nelim b1; nelim b2; nelim b3; nnormalize; napply refl_eq. nqed.
+nlemma andb_false5_5 : ∀b1,b2,b3,b4.(b1 ⊗ b2 ⊗ b3 ⊗ b4 ⊗ false) = false.
+ #b1; #b2; #b3; #b4; nelim b1; nelim b2; nelim b3; nelim b4; nnormalize; napply refl_eq. nqed.
+
nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
#b1; #b2;
ncases b1;
#x; nelim x; #e1; #e2;
#y; nelim y; #e3; #e4;
nnormalize;
- napply (or_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_b8_aux1 e1 e2 e3 e4 H))
- ##| ##1: #H; napply (or_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
- ##[ ##2: #H1; napply (or_intror … (decidable_b8_aux2 e1 e2 e3 e4 H1))
+ napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_b8_aux1 e1 e2 e3 e4 H))
+ ##| ##1: #H; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_b8_aux2 e1 e2 e3 e4 H1))
##| ##1: #H1; nrewrite > H; nrewrite > H1;
- napply (or_introl … (refl_eq ? 〈e3,e4〉))
+ napply (or2_intro1 … (refl_eq ? 〈e3,e4〉))
##]
##]
nqed.
#e1; #e2; #e3; #e4;
nchange with ((((eq_ex e3 e1) ⊗ (eq_ex e4 e2)) = false) → ?);
#H;
- napply (or_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false … H) …);
##[ ##1: #H1; napply (decidable_b8_aux1 … (neqex_to_neq … H1))
##| ##2: #H1; napply (decidable_b8_aux2 … (neqex_to_neq … H1))
##]
nlemma byte8_destruct : ∀e1,e2,e3,e4.〈e1,e2〉 ≠ 〈e3,e4〉 → e1 ≠ e3 ∨ e2 ≠ e4.
#e1; #e2; #e3; #e4;
nnormalize; #H;
- napply (or_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (or_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
- ##[ ##2: #H2; napply (or_intror … H2)
+ napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
+ ##[ ##2: #H2; napply (or2_intro2 … H2)
##| ##1: #H2; nrewrite > H1 in H:(%);
nrewrite > H2;
#H; nelim (H (refl_eq …))
nelim b1; #e1; #e2;
nelim b2; #e3; #e4;
#H; nchange with (((eq_ex e1 e3) ⊗ (eq_ex e2 e4)) = false);
- napply (or_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …);
+ napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …);
##[ ##1: #H1; nrewrite > (neq_to_neqex … H1); nnormalize; napply refl_eq
##| ##2: #H1; nrewrite > (neq_to_neqex … H1);
nrewrite > (symmetric_andbool (eq_ex e1 e3) false);
ndefinition exadecim_destruct_aux ≝
Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
match e1 with
- [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
- | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
- | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ]
- | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
- | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ]
- | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
- | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ]
- | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
- | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ]
- | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
- | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ]
- | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
- | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ]
- | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
- | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
- | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
+ [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
+ | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
+ | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
+ | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
+ | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
+ | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
+ | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
+ | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
].
ndefinition exadecim_destruct : exadecim_destruct_aux.
#e1; ncases e1;
- ##[ ##1: napply exadecim_destruct1
- ##| ##2: napply exadecim_destruct2
- ##| ##3: napply exadecim_destruct3
- ##| ##4: napply exadecim_destruct4
- ##| ##5: napply exadecim_destruct5
- ##| ##6: napply exadecim_destruct6
- ##| ##7: napply exadecim_destruct7
- ##| ##8: napply exadecim_destruct8
- ##| ##9: napply exadecim_destruct9
- ##| ##10: napply exadecim_destruct10
- ##| ##11: napply exadecim_destruct11
- ##| ##12: napply exadecim_destruct12
- ##| ##13: napply exadecim_destruct13
- ##| ##14: napply exadecim_destruct14
- ##| ##15: napply exadecim_destruct15
- ##| ##16: napply exadecim_destruct16
+ ##[ ##1: napply exadecim_destruct1 ##| ##2: napply exadecim_destruct2
+ ##| ##3: napply exadecim_destruct3 ##| ##4: napply exadecim_destruct4
+ ##| ##5: napply exadecim_destruct5 ##| ##6: napply exadecim_destruct6
+ ##| ##7: napply exadecim_destruct7 ##| ##8: napply exadecim_destruct8
+ ##| ##9: napply exadecim_destruct9 ##| ##10: napply exadecim_destruct10
+ ##| ##11: napply exadecim_destruct11 ##| ##12: napply exadecim_destruct12
+ ##| ##13: napply exadecim_destruct13 ##| ##14: napply exadecim_destruct14
+ ##| ##15: napply exadecim_destruct15 ##| ##16: napply exadecim_destruct16
##]
nqed.
napply refl_eq.
nqed.
+nlemma associative_andex1 : ∀e2,e3.(and_ex (and_ex x0 e2) e3) = (and_ex x0 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex2 : ∀e2,e3.(and_ex (and_ex x1 e2) e3) = (and_ex x1 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex3 : ∀e2,e3.(and_ex (and_ex x2 e2) e3) = (and_ex x2 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex4 : ∀e2,e3.(and_ex (and_ex x3 e2) e3) = (and_ex x3 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex5 : ∀e2,e3.(and_ex (and_ex x4 e2) e3) = (and_ex x4 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex6 : ∀e2,e3.(and_ex (and_ex x5 e2) e3) = (and_ex x5 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex7 : ∀e2,e3.(and_ex (and_ex x6 e2) e3) = (and_ex x6 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex8 : ∀e2,e3.(and_ex (and_ex x7 e2) e3) = (and_ex x7 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex9 : ∀e2,e3.(and_ex (and_ex x8 e2) e3) = (and_ex x8 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex10 : ∀e2,e3.(and_ex (and_ex x9 e2) e3) = (and_ex x9 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex11 : ∀e2,e3.(and_ex (and_ex xA e2) e3) = (and_ex xA (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex12 : ∀e2,e3.(and_ex (and_ex xB e2) e3) = (and_ex xB (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex13 : ∀e2,e3.(and_ex (and_ex xC e2) e3) = (and_ex xC (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex14 : ∀e2,e3.(and_ex (and_ex xD e2) e3) = (and_ex xD (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex15 : ∀e2,e3.(and_ex (and_ex xE e2) e3) = (and_ex xE (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_andex16 : ∀e2,e3.(and_ex (and_ex xF e2) e3) = (and_ex xF (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+
nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
- #e1; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ #e1; nelim e1;
+ ##[ ##1: napply associative_andex1 ##| ##2: napply associative_andex2
+ ##| ##3: napply associative_andex3 ##| ##4: napply associative_andex4
+ ##| ##5: napply associative_andex5 ##| ##6: napply associative_andex6
+ ##| ##7: napply associative_andex7 ##| ##8: napply associative_andex8
+ ##| ##9: napply associative_andex9 ##| ##10: napply associative_andex10
+ ##| ##11: napply associative_andex11 ##| ##12: napply associative_andex12
+ ##| ##13: napply associative_andex13 ##| ##14: napply associative_andex14
+ ##| ##15: napply associative_andex15 ##| ##16: napply associative_andex16
##]
nqed.
napply refl_eq.
nqed.
+nlemma associative_orex1 : ∀e2,e3.(or_ex (or_ex x0 e2) e3) = (or_ex x0 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex2 : ∀e2,e3.(or_ex (or_ex x1 e2) e3) = (or_ex x1 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex3 : ∀e2,e3.(or_ex (or_ex x2 e2) e3) = (or_ex x2 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex4 : ∀e2,e3.(or_ex (or_ex x3 e2) e3) = (or_ex x3 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex5 : ∀e2,e3.(or_ex (or_ex x4 e2) e3) = (or_ex x4 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex6 : ∀e2,e3.(or_ex (or_ex x5 e2) e3) = (or_ex x5 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex7 : ∀e2,e3.(or_ex (or_ex x6 e2) e3) = (or_ex x6 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex8 : ∀e2,e3.(or_ex (or_ex x7 e2) e3) = (or_ex x7 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex9 : ∀e2,e3.(or_ex (or_ex x8 e2) e3) = (or_ex x8 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex10 : ∀e2,e3.(or_ex (or_ex x9 e2) e3) = (or_ex x9 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex11 : ∀e2,e3.(or_ex (or_ex xA e2) e3) = (or_ex xA (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex12 : ∀e2,e3.(or_ex (or_ex xB e2) e3) = (or_ex xB (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex13 : ∀e2,e3.(or_ex (or_ex xC e2) e3) = (or_ex xC (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex14 : ∀e2,e3.(or_ex (or_ex xD e2) e3) = (or_ex xD (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex15 : ∀e2,e3.(or_ex (or_ex xE e2) e3) = (or_ex xE (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_orex16 : ∀e2,e3.(or_ex (or_ex xF e2) e3) = (or_ex xF (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+
nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
- #e1; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ #e1; nelim e1;
+ ##[ ##1: napply associative_orex1 ##| ##2: napply associative_orex2
+ ##| ##3: napply associative_orex3 ##| ##4: napply associative_orex4
+ ##| ##5: napply associative_orex5 ##| ##6: napply associative_orex6
+ ##| ##7: napply associative_orex7 ##| ##8: napply associative_orex8
+ ##| ##9: napply associative_orex9 ##| ##10: napply associative_orex10
+ ##| ##11: napply associative_orex11 ##| ##12: napply associative_orex12
+ ##| ##13: napply associative_orex13 ##| ##14: napply associative_orex14
+ ##| ##15: napply associative_orex15 ##| ##16: napply associative_orex16
##]
nqed.
napply refl_eq.
nqed.
+nlemma associative_xorex1 : ∀e2,e3.(xor_ex (xor_ex x0 e2) e3) = (xor_ex x0 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex2 : ∀e2,e3.(xor_ex (xor_ex x1 e2) e3) = (xor_ex x1 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex3 : ∀e2,e3.(xor_ex (xor_ex x2 e2) e3) = (xor_ex x2 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex4 : ∀e2,e3.(xor_ex (xor_ex x3 e2) e3) = (xor_ex x3 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex5 : ∀e2,e3.(xor_ex (xor_ex x4 e2) e3) = (xor_ex x4 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex6 : ∀e2,e3.(xor_ex (xor_ex x5 e2) e3) = (xor_ex x5 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex7 : ∀e2,e3.(xor_ex (xor_ex x6 e2) e3) = (xor_ex x6 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex8 : ∀e2,e3.(xor_ex (xor_ex x7 e2) e3) = (xor_ex x7 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex9 : ∀e2,e3.(xor_ex (xor_ex x8 e2) e3) = (xor_ex x8 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex10 : ∀e2,e3.(xor_ex (xor_ex x9 e2) e3) = (xor_ex x9 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex11 : ∀e2,e3.(xor_ex (xor_ex xA e2) e3) = (xor_ex xA (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex12 : ∀e2,e3.(xor_ex (xor_ex xB e2) e3) = (xor_ex xB (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex13 : ∀e2,e3.(xor_ex (xor_ex xC e2) e3) = (xor_ex xC (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex14 : ∀e2,e3.(xor_ex (xor_ex xD e2) e3) = (xor_ex xD (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex15 : ∀e2,e3.(xor_ex (xor_ex xE e2) e3) = (xor_ex xE (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_xorex16 : ∀e2,e3.(xor_ex (xor_ex xF e2) e3) = (xor_ex xF (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+
nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
- #e1; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ #e1; nelim e1;
+ ##[ ##1: napply associative_xorex1 ##| ##2: napply associative_xorex2
+ ##| ##3: napply associative_xorex3 ##| ##4: napply associative_xorex4
+ ##| ##5: napply associative_xorex5 ##| ##6: napply associative_xorex6
+ ##| ##7: napply associative_xorex7 ##| ##8: napply associative_xorex8
+ ##| ##9: napply associative_xorex9 ##| ##10: napply associative_xorex10
+ ##| ##11: napply associative_xorex11 ##| ##12: napply associative_xorex12
+ ##| ##13: napply associative_xorex13 ##| ##14: napply associative_xorex14
+ ##| ##15: napply associative_xorex15 ##| ##16: napply associative_xorex16
##]
nqed.
napply refl_eq.
nqed.
+nlemma associative_plusex_d_d1 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x0 e2) e3) = (plus_ex_d_d x0 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d2 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x1 e2) e3) = (plus_ex_d_d x1 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d3 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x2 e2) e3) = (plus_ex_d_d x2 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d4 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x3 e2) e3) = (plus_ex_d_d x3 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d5 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x4 e2) e3) = (plus_ex_d_d x4 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d6 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x5 e2) e3) = (plus_ex_d_d x5 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d7 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x6 e2) e3) = (plus_ex_d_d x6 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d8 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x7 e2) e3) = (plus_ex_d_d x7 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d9 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x8 e2) e3) = (plus_ex_d_d x8 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d10 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x9 e2) e3) = (plus_ex_d_d x9 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d11 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xA e2) e3) = (plus_ex_d_d xA (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d12 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xB e2) e3) = (plus_ex_d_d xB (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d13 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xC e2) e3) = (plus_ex_d_d xC (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d14 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xD e2) e3) = (plus_ex_d_d xD (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d15 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xE e2) e3) = (plus_ex_d_d xE (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+nlemma associative_plusex_d_d16 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xF e2) e3) = (plus_ex_d_d xF (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
+
nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)).
- #e1; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ #e1; nelim e1;
+ ##[ ##1: napply associative_plusex_d_d1 ##| ##2: napply associative_plusex_d_d2
+ ##| ##3: napply associative_plusex_d_d3 ##| ##4: napply associative_plusex_d_d4
+ ##| ##5: napply associative_plusex_d_d5 ##| ##6: napply associative_plusex_d_d6
+ ##| ##7: napply associative_plusex_d_d7 ##| ##8: napply associative_plusex_d_d8
+ ##| ##9: napply associative_plusex_d_d9 ##| ##10: napply associative_plusex_d_d10
+ ##| ##11: napply associative_plusex_d_d11 ##| ##12: napply associative_plusex_d_d12
+ ##| ##13: napply associative_plusex_d_d13 ##| ##14: napply associative_plusex_d_d14
+ ##| ##15: napply associative_plusex_d_d15 ##| ##16: napply associative_plusex_d_d16
##]
nqed.
nnormalize;
nelim x;
nelim y;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H)
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H)
##]
nqed.
nnormalize;
nelim x;
nelim y;
- ##[ ##1,10,19,28,37,46,55,64: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (oct_destruct … H)
+ ##[ ##1,10,19,28,37,46,55,64: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (oct_destruct … H)
##]
nqed.
nnormalize;
nelim x;
nelim y;
- ##[ ##1,6,11,16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (quatern_destruct … H)
+ ##[ ##1,6,11,16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (quatern_destruct … H)
##]
nqed.
#x; nelim x; #b1; #b2;
#y; nelim y; #b3; #b4;
nnormalize;
- napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_w16_aux1 b1 b2 b3 b4 H))
- ##| ##1: #H; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
- ##[ ##2: #H1; napply (or_intror … (decidable_w16_aux2 b1 b2 b3 b4 H1))
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w16_aux1 b1 b2 b3 b4 H))
+ ##| ##1: #H; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+ ##[ ##2: #H1; napply (or2_intro2 … (decidable_w16_aux2 b1 b2 b3 b4 H1))
##| ##1: #H1; nrewrite > H; nrewrite > H1;
- napply (or_introl … (refl_eq ? 〈b3:b4〉))
+ napply (or2_intro1 … (refl_eq ? 〈b3:b4〉))
##]
##]
nqed.
#b1; #b2; #b3; #b4;
nchange with ((((eq_b8 b3 b1) ⊗ (eq_b8 b4 b2)) = false) → ?);
#H;
- napply (or_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …);
##[ ##1: #H1; napply (decidable_w16_aux1 … (neqb8_to_neq … H1))
##| ##2: #H1; napply (decidable_w16_aux2 … (neqb8_to_neq … H1))
##]
nlemma word16_destruct : ∀b1,b2,b3,b4.〈b1:b2〉 ≠ 〈b3:b4〉 → b1 ≠ b3 ∨ b2 ≠ b4.
#b1; #b2; #b3; #b4;
nnormalize; #H;
- napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
- ##[ ##2: #H2; napply (or_intror … H2)
+ napply (or2_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+ ##[ ##2: #H2; napply (or2_intro2 … H2)
##| ##1: #H2; nrewrite > H1 in H:(%);
nrewrite > H2;
#H; nelim (H (refl_eq …))
nelim w1; #b1; #b2;
nelim w2; #b3; #b4;
#H; nchange with (((eq_b8 b1 b3) ⊗ (eq_b8 b2 b4)) = false);
- napply (or_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …);
+ napply (or2_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …);
##[ ##1: #H1; nrewrite > (neq_to_neqb8 … H1); nnormalize; napply refl_eq
##| ##2: #H1; nrewrite > (neq_to_neqb8 … H1);
nrewrite > (symmetric_andbool (eq_b8 b1 b3) false);
#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);
projects / helm.git / commitdiff