Changeset 2292 for src/utilities


Ignore:
Timestamp:
Aug 2, 2012, 6:40:15 PM (8 years ago)
Author:
campbell
Message:

More RTLabs invariants.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1949 r2292  
    7676[ * [ // | #h #t #_ * ]
    7777| #ha #ta #IH * [ // | #hb #tb #H * #H1 #H2 % [ @H @H1 | @(IH … H2) @H ] ]
     78] qed.
     79
     80lemma All2_left : ∀A,B,P,la,lb.
     81  All2 A B P la lb → All A (λa.∃b.P a b) la.
     82#A #B #P #la elim la
     83[ //
     84| #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hdb} // | /2/ ]
     85] qed.
     86
     87lemma All2_right : ∀A,B,P,la,lb.
     88  All2 A B P la lb → All B (λb.∃a.P a b) lb.
     89#A #B #P #la elim la
     90[ * // #h #t *
     91| #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} // | /2/ ]
    7892] qed.
    7993
Note: See TracChangeset for help on using the changeset viewer.