Changeset 2273 for src/ASM/AssemblyProofSplitSplit.ma
- Timestamp:
- Jul 30, 2012, 12:46:19 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplitSplit.ma
r2269 r2273 51 51 qed. 52 52 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 v158 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%59 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ260 #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]61 qed.62 63 53 theorem main_thm: 64 54 ∀M, M': internal_pseudo_address_map.
Note: See TracChangeset
for help on using the changeset viewer.