Changeset 1521 for src/RTLabs/RTLabsToRTL.ma
 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.