Changeset 2190 for src

Timestamp:

Jul 17, 2012, 1:41:49 AM (9 years ago)

Author:

sacerdot

Message:

Two daemons left.

File:

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

src/ASM/Assembly.ma

@@ -1040 +1040 @@
       @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
       @pair_elim #len' #assembledi' #eq_assembly_1_pseudoinstruction #IH
-      cases (IH ?)
-      [2: cases daemon (*CSC: new proof obligation*) ] #IH6 #IH
+      cases (IH ?) -IH
+      [2: %1 cases OR_lt_eq
+        [ normalize nodelta >nat_of_bitvector_add
+          [2: cases daemon (*CSC: should be true*)]
+          >nat_of_bitvector_bitvector_of_nat_inverse [2: // ]
+          <plus_n_Sm <plus_n_O #X lapply (le_S_S_to_le … X) -X #X
+          cases (le_to_or_lt_eq … X) [//] #abs @⊥
+          lapply (eq_f … (bitvector_of_nat 16) … abs)
+          >bitvector_of_nat_inverse_nat_of_bitvector
+          >bitvector_of_nat_inverse_nat_of_bitvector #EQ
+          @(absurd … EQ NEQppc')
+        | >length_append <plus_n_Sm <plus_n_O #EQ @le_S_S_to_le >IH1
+          >nat_of_bitvector_bitvector_of_nat_inverse try assumption
+          cases (le_to_or_lt_eq … (lt_nat_of_bitvector 16 ppc')) [#X >EQ @X]
+          #abs @⊥ <EQ in abs; #X lapply (injective_S … X) #abs
+          lapply (eq_f … (bitvector_of_nat 16) … abs)
+          >bitvector_of_nat_inverse_nat_of_bitvector <IH1 #EQ
+          @(absurd … EQ NEQppc') ]]
+      #IH6 #IH
       change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ? ∧ ∀j:ℕ. ∀H:j<|assembledi|.?)
       >eq_assembly_1_pseudoinstruction %
-      [ cases daemon (*CSC: new proof obligation*)
+      [ >reverse_append >length_append
+        >(fst_snd_assembly_1_pseudoinstruction … eq_assembly_1_pseudoinstruction)
+        @(transitive_le … IH6) //
       | #j #LTj >reverse_append >reverse_reverse #K
         >IH