matita/matita/contribs/lambdadelta/delayed_updating/etc/path_etc.etc

   1 notation "hvbox( l1 ● break l2 )"
   2   right associative with precedence 47
   3   for @{ 'DoubleSemicolon $l1 $l2 }.
   4
   5 notation "hvbox( hd ◗ break tl )"
   6   right associative with precedence 47
   7   for @{ 'Semicolon $hd $tl }.
   8
   9 notation "hvbox( hd ◖ break tl )"
  10   left associative with precedence 47
  11   for @{ 'Comma $hd $tl }.
  12
  13 lemma tmp1 (l1) (l2) (p): l1 ◗ l2 ◗ p = l1 ◗ (l2 ◗ p).
  14 // qed.
  15
  16 lemma tmp2 (p) (l1) (l2): p ◖ l1 ◖ l2 = (p ◖ l1) ◖ l2.
  17 // qed.
  18
  19 lemma tmp3 (p1) (p2) (p3): p1 ● p2 ● p3 = p1 ● (p2 ● p3).
  20 // qed.
  21
  22 lemma tmp4 (l1) (p) (l2): l1 ◗ p ◖ l2 = l1 ◗ (p ◖ l2).
  23 // qed.
  24
  25 lemma tmp5 (p1) (l) (p2): p1 ◖ l ● p2 = (p1 ◖ l) ● p2.
  26 // qed.
  27
  28 lemma tmp6 (p1) (p2) (l): p1 ● p2 ◖ l  = p1 ● (p2 ◖ l).
  29 // qed.
  30
  31 lemma tmp7 (l) (p1) (p2): l ◗ p1 ● p2 = l ◗ (p1 ● p2).
  32 // qed.
  33
  34 lemma tmp8 (p1) (l) (p2): p1 ● l ◗ p2 = p1 ● (l ◗ p2).
  35 // qed.