Changeset 2702 for src/ASM/UtilBranch.ma
- Timestamp:
- Feb 22, 2013, 3:27:16 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/UtilBranch.ma
r1946 r2702 24 24 >inductive_hypothesis 25 25 >inductive_hypothesis 26 [1: 27 change with ( 28 ? + (2 * buffer + 1) * ?) in ⊢ (??%?); 29 change with ( 30 ? + buffer * (2 * 2^n')) in ⊢ (???%); 31 cases daemon 32 ] 33 ] 34 cases daemon 26 [1: change with (? + (2 * buffer + 1) * ?) in ⊢ (??%?); 27 >associative_plus in ⊢ (???%); @eq_f >commutative_plus 28 whd in ⊢ (??%?); @eq_f2 // >commutative_times in ⊢ (???(??%)); 29 <associative_times // 30 | <plus_n_O normalize <plus_n_O @eq_f <associative_times 31 <commutative_times in ⊢ (???%); <associative_times // 35 32 qed. 36 33
Note: See TracChangeset
for help on using the changeset viewer.