- Timestamp:
- Jul 17, 2012, 1:41:49 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2189 r2190 1040 1040 @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction 1041 1041 @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH 1042 cases (IH ?) 1043 [2: cases daemon (*CSC: new proof obligation*) ] #IH6 #IH 1042 cases (IH ?) -IH 1043 [2: %1 cases OR_lt_eq 1044 [ normalize nodelta >nat_of_bitvector_add 1045 [2: cases daemon (*CSC: should be true*)] 1046 >nat_of_bitvector_bitvector_of_nat_inverse [2: // ] 1047 <plus_n_Sm <plus_n_O #X lapply (le_S_S_to_le … X) -X #X 1048 cases (le_to_or_lt_eq … X) [//] #abs @⊥ 1049 lapply (eq_f … (bitvector_of_nat 16) … abs) 1050 >bitvector_of_nat_inverse_nat_of_bitvector 1051 >bitvector_of_nat_inverse_nat_of_bitvector #EQ 1052 @(absurd … EQ NEQppc') 1053 | >length_append <plus_n_Sm <plus_n_O #EQ @le_S_S_to_le >IH1 1054 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 1055 cases (le_to_or_lt_eq … (lt_nat_of_bitvector 16 ppc')) [#X >EQ @X] 1056 #abs @⊥ <EQ in abs; #X lapply (injective_S … X) #abs 1057 lapply (eq_f … (bitvector_of_nat 16) … abs) 1058 >bitvector_of_nat_inverse_nat_of_bitvector <IH1 #EQ 1059 @(absurd … EQ NEQppc') ]] 1060 #IH6 #IH 1044 1061 change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ? ∧ ∀j:ℕ. ∀H:j<|assembledi|.?) 1045 1062 >eq_assembly_1_pseudoinstruction % 1046 [ cases daemon (*CSC: new proof obligation*) 1063 [ >reverse_append >length_append 1064 >(fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction) 1065 @(transitive_le … IH6) // 1047 1066 | #j #LTj >reverse_append >reverse_reverse #K 1048 1067 >IH
Note: See TracChangeset
for help on using the changeset viewer.