Ignore:
Timestamp:
Feb 1, 2012, 4:16:06 PM (7 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/CexecSound.ma

    r1647 r1672  
    285285    | #a #b #c #d #e #bad destruct (bad);
    286286    | #a #b #c #d #e #f #g #h #bad destruct (bad);
    287     | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad @False_ind destruct (bad);
    288     | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
     287    | #a #b #c #d #e #f #g #h #i #j #k #l #bad @False_ind destruct (bad);
     288    | #a #b #c #d #e #f #g #h #i #j #bad destruct (bad);
    289289    ]
    290290| #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
    291 | #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    292 | #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
    293 | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
    294 | #a #b #c #d #e #f #g #h #i #j #k #l #m #bad destruct (bad);
    295291| #a #b #c #d #e #f #g #h #bad destruct (bad);
    296 | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad destruct (bad);
     292| #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
     293| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
     294| #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
     295| #a #b #c #d #e #f #g #bad destruct (bad);
     296| #a #b #c #d #e #f #g #h #i #j #k #l #bad destruct (bad);
     297| #a #b #c #d #e #f #g #bad destruct (bad);
     298| #a #b #c #d #e #f #g #h #i #j #k #l #bad  destruct (bad);
    297299| #a #b #c #d #e #f #g #h #bad destruct (bad);
    298 | #a #b #c #d #e #f #g #h #i #j #k #l #m #n #bad  destruct (bad);
    299 | #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    300 | #a #b #c #d #e #f #g #bad destruct (bad);
     300| #a #b #c #d #e #f #bad destruct (bad);
    301301] qed.
    302302
Note: See TracChangeset for help on using the changeset viewer.