Changeset 2702 for src/ASM/UtilBranch.ma


Ignore:
Timestamp:
Feb 22, 2013, 3:27:16 PM (7 years ago)
Author:
sacerdot
Message:
  1. proof closed in ASM/UtilBranch
  2. more passes integrated in the compiler.ma
  3. some work on commenting out broken proofs in linearise.ma
File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/UtilBranch.ma

    r1946 r2702  
    2424    >inductive_hypothesis
    2525    >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 //
    3532qed.
    3633
Note: See TracChangeset for help on using the changeset viewer.