1 notation "hvbox( l1 ● break l2 )"
2 right associative with precedence 47
3 for @{ 'DoubleSemicolon $l1 $l2 }.
5 notation "hvbox( hd ◗ break tl )"
6 right associative with precedence 47
7 for @{ 'Semicolon $hd $tl }.
9 notation "hvbox( hd ◖ break tl )"
10 left associative with precedence 47
11 for @{ 'Comma $hd $tl }.
13 lemma tmp1 (l1) (l2) (p): l1 ◗ l2 ◗ p = l1 ◗ (l2 ◗ p).
16 lemma tmp2 (p) (l1) (l2): p ◖ l1 ◖ l2 = (p ◖ l1) ◖ l2.
19 lemma tmp3 (p1) (p2) (p3): p1 ● p2 ● p3 = p1 ● (p2 ● p3).
22 lemma tmp4 (l1) (p) (l2): l1 ◗ p ◖ l2 = l1 ◗ (p ◖ l2).
25 lemma tmp5 (p1) (l) (p2): p1 ◖ l ● p2 = (p1 ◖ l) ● p2.
28 lemma tmp6 (p1) (p2) (l): p1 ● p2 ◖ l = p1 ● (p2 ◖ l).
31 lemma tmp7 (l) (p1) (p2): l ◗ p1 ● p2 = l ◗ (p1 ● p2).
34 lemma tmp8 (p1) (l) (p2): p1 ● l ◗ p2 = p1 ● (l ◗ p2).