Changeset 2190


Ignore:
Timestamp:
Jul 17, 2012, 1:41:49 AM (5 years ago)
Author:
sacerdot
Message:

Two daemons left.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2189 r2190  
    10401040      @pair_elim #pi' #newppc' #eq_fetch_pseudoinstruction
    10411041      @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
    10441061      change with (let 〈len,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi' in ? ∧ ∀j:ℕ. ∀H:j<|assembledi|.?)
    10451062      >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) //
    10471066      | #j #LTj >reverse_append >reverse_reverse #K
    10481067        >IH
Note: See TracChangeset for help on using the changeset viewer.