Changeset 2073


Ignore:
Timestamp:
Jun 14, 2012, 4:10:45 AM (5 years ago)
Author:
sacerdot
Message:

All false daemons removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2072 r2073  
    826826    >EQignore_revcode in Hfold; * * #Hfold1 #Hfold3 #Hfold2 whd >p1 whd #ppc #LTppc @Hfold2
    827827    >Hfold1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    828     (* CSC: FALSE, NEEDS ADDITIONAL ASSUMPTION *) cases daemon
     828    <p_refl in instr_list_ok; #H @H
    829829  | %
    830830    [ % // (*CSC: NEW INVARIANT FOR JAAP!*) cases daemon ]
     
    849849        >nat_of_bitvector_bitvector_of_nat_inverse
    850850        [2,4: (* CSC: TRUE, NEEDS LEMMA, MAYBE ALREADY PROVED *) cases daemon
    851         |3: (* CSC: TRUE, NEEDS INVARIANT *) cases daemon ]
    852         >reverse_append >reverse_reverse
    853         (* CSC: TRUE, NEEDS SAME INVARIANT *)
    854         >(? : nat_of_bitvector … (sigma ppc) = |reverse … code|) [2: cases daemon]
     851        |3: (*CSC: TRUE, NEEDS LEMMA *) cases daemon ]
     852        >reverse_append >reverse_reverse >IH3 <(length_reverse … code)
    855853        @nth_safe_prepend
    856854    | #LTppc''
     
    878876      >eq_assembly_1_pseudoinstruction #j #LTj >reverse_append >reverse_reverse #K
    879877      >IH
    880       [2: >length_reverse <IH3 (*CSC: FALSE, WE CAN PROVE PPC'<=PPC, SO WHAT? *) cases daemon
     878      [2: >length_reverse <IH3 (*CSC: NEEDS JAAP INVARIANT PLUS SOME WORK *) cases daemon
    881879      | @shift_nth_prefix
    882880      |3: @le_S_S_to_le @(transitive_le … LTppc'') >nat_of_bitvector_add
Note: See TracChangeset for help on using the changeset viewer.