Changeset 1521 for src/RTLabs
- Timestamp:
- Nov 21, 2011, 1:06:01 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r1515 r1521 32 32 |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|. 33 33 #globals #def #left #right 34 whd in match complete_regs normalize nodelta34 whd in match complete_regs; normalize nodelta 35 35 @leb_elim normalize nodelta #H 36 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right))) 37 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left))) ]36 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right))); 37 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)));] 38 38 cases (fresh_regs ????) #def' #fresh normalize >append_length 39 generalize in match H -H;40 generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)41 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus39 generalize in match H; -H; 40 generalize in match (length … left); generalize in match (length … right); generalize in match (length … fresh); 41 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H); -H #H #E >E >commutative_plus 42 42 <plus_minus_m_m /2/ ] 43 43 qed.
Note: See TracChangeset
for help on using the changeset viewer.