Changeset 831


Ignore:
Timestamp:
May 24, 2011, 4:01:41 PM (8 years ago)
Author:
sacerdot
Message:

Progress in proofs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r829 r831  
    8989     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
    9090       cases (split ????) #z1 #z2 %
     91     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
     92       cases (split ????) #z1 #z2 %
     93     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
     94       cases (split ????) #z1 #z2 %
     95     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
    9196     | *: cases not_implemented
    9297     ]
     
    9499  | #cost %
    95100  | #label %
    96   | #label (* CSC: ??? *)
     101  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
     102    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
     103    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
     104    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
     105    (* CSC: ??? *)
    97106  | #dptr #label (* CSC: ??? *)
    98107  ]
Note: See TracChangeset for help on using the changeset viewer.