Ignore:
Timestamp:
Feb 1, 2012, 4:16:06 PM (8 years ago)
Author:
campbell
Message:

Matita now generates a couple of inversion lemmas that were manually
proved before.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1603 r1672  
    124124#ge #env #m #e #ty #l #ofs #tr #P #H @(eval_lvalue_inv_ind … H)
    125125[ #id #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 destruct; //
    126 | #id #sp #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
    127 | #e' #ty' #sp #l' #ofs #tr #H #e1 #e2 #e3 #e4 #e5 destruct; //
    128 | #e' #id #ty' #l' #ofs #id' #fs #d #tr #H #e1 #e2 (* bogus? *) #_ #e3 #e4 #e5 #e6 #e7 destruct; //
    129 | #e' #id #ty' #l' #ofs #id' #fs #tr #H #e1 (* bogus? *) #_ #e2 #e3 #e4 #e5 #e6 destruct; //
     126| #id #l' #ty' #e1 #e2 #e3 #e4 #e5 #e6 #e7 destruct; //
     127| #e' #ty' #sp #l' #pc #ofs #tr #H' #e1 #e2 #e3 #e4 #e5 -H destruct; //
     128| #e' #id #ty' #l' #ofs #id' #fs #d #tr #H' #e1 #e2 #e3 #e4 #e5 #e6 #e7 -H destruct; //
     129| #e' #id #ty' #l' #ofs #id' #fs #tr #H' #e1 #e2 #e3 #e4 #e5 #e6 -H destruct; //
    130130] qed.
    131131
Note: See TracChangeset for help on using the changeset viewer.