Ignore:
Timestamp:
Jul 30, 2012, 12:46:19 AM (7 years ago)
Author:
sacerdot
Message:
  1. lemmas moved from all files to Test.ma
  2. most of the lemmas in Test.ma repaired. A few are commented out. Several needs to be slightly generalized.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2269 r2273  
    5151qed.
    5252
    53 (*CSC: move elsewhere*)
    54 lemma bv_append_eq_to_eq:
    55  ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
    56   v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
    57  #A #n #v1 elim v1
    58  [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
    59  | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
    60    #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
    61 qed.
    62    
    6353theorem main_thm:
    6454  ∀M, M': internal_pseudo_address_map.
Note: See TracChangeset for help on using the changeset viewer.