Changeset 2273 for src/ASM/AssemblyProofSplitSplit.ma

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:

• src/ASM/AssemblyProofSplitSplit.ma (modified) (1 diff)

src/ASM/AssemblyProofSplitSplit.ma

@@ -51 +51 @@
 qed.
 
-(*CSC: move elsewhere*)
-lemma bv_append_eq_to_eq:
- ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
-  v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
- #A #n #v1 elim v1
- [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
- | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
-   #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
-qed.
-   
 theorem main_thm:
   ∀M, M': internal_pseudo_address_map.