notation "i ◂ e" left associative with precedence 60 for @{'ltrif $i $e}.
interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e).
notation "i ◂ e" left associative with precedence 60 for @{'ltrif $i $e}.
interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e).
[ true ⇒ (i1 ◂ (bcast ? i2))
| false ⇒ 〈i1 · i2,false〉
]
[ true ⇒ (i1 ◂ (bcast ? i2))
| false ⇒ 〈i1 · i2,false〉
]
notation "a ▸ b" left associative with precedence 60 for @{'lc eclose $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
definition lk ≝ λS:DeqSet.λbcast:∀S:DeqSet.∀E:pitem S.pre S.λe:pre S.
match e with
notation "a ▸ b" left associative with precedence 60 for @{'lc eclose $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
definition lk ≝ λS:DeqSet.λbcast:∀S:DeqSet.∀E:pitem S.pre S.λe:pre S.
match e with
lemma erase_odot:∀S.∀e1,e2:pre S.
|\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
lemma erase_odot:∀S.∀e1,e2:pre S.
|\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).