Qcert.NRAEnv.Optim.TNRAEnvRewrite
Section TOptimEnv.
Context {m:basic_model}.
Lemma tand_comm_arrow (q₁ q₂:cnraenv) :
q₁ ∧ q₂ ⇒ q₂ ∧ q₁.
Lemma tand_comm {τc τenv τin} (q₁ q₂ ql qr: m ⊧ τin ⇝ Bool ⊣ τc;τenv) :
(`ql = `q₂ ∧ `q₁) →
(`qr = `q₁ ∧ `q₂) →
ql ≡τ qr.
Lemma tconcat_empty_record_r_arrow q:
q ⊕ ‵[||] ⇒ q.
Lemma tconcat_empty_record_l_arrow q:
‵[||] ⊕ q ⇒ q.
Lemma tmerge_empty_record_r_arrow q:
q ⊗ ‵[||] ⇒ ‵{| q |}.
Lemma tmerge_empty_record_l_arrow q:
‵[||] ⊗ q ⇒ ‵{| q |}.
Lemma tdot_over_rec_arrow a q :
(‵[| (a, q)|]) · a ⇒ q.
Lemma tdot_over_concat_eq_r_arrow a (q₁ q₂:cnraenv) :
(q₁ ⊕ ‵[| (a, q₂) |])·a ⇒ q₂.
Lemma tdot_over_concat_neq_r_arrow a₁ a₂ (q₁ q₂:cnraenv) :
a₁ ≠ a₂ →
(q₁ ⊕ ‵[| (a₁, q₂) |])·a₂ ⇒ q₁·a₂.
Lemma tdot_over_concat_neq_l_arrow a₁ a₂ (q₁ q₂:cnraenv) :
a₁ ≠ a₂ →
(‵[| (a₁, q₁) |] ⊕ q₂ )·a₂ ⇒ q₂·a₂.
Lemma tenvdot_from_duplicate_r_arrow a₁ a₂ (q₁ q₂:cnraenv) :
(‵[| (a₁, q₁) |] ⊕ ‵[| (a₂, q₂) |])·a₂ ⇒ q₂.
Lemma tenvdot_from_duplicate_l_arrow a₁ a₂ (q₁ q₂:cnraenv) :
a₁ ≠ a₂ → (‵[| (a₁, q₁) |] ⊕ ‵[| (a₂, q₂) |])·a₁ ⇒ q₁.
Lemma tproduct_singletons_arrow a₁ a₂ q₁ q₂:
‵{|‵[| (a₁, q₁) |] |} × ‵{| ‵[| (a₂, q₂) |] |} ⇒
‵{|‵[| (a₁, q₁) |] ⊕ ‵[| (a₂, q₂) |] |}.
Lemma tproduct_empty_right_arrow q:
q × ‵{| ‵[||] |} ⇒ q.
Lemma tproduct_empty_left_arrow q:
‵{| ‵[||] |} × q ⇒ q.
Lemma tconcat_over_rec_eq s p₁ p₂ :
‵[| (s, p₁) |] ⊕ ‵[| (s, p₂) |] ⇒ ‵[| (s, p₂) |].
Lemma tmerge_concat_to_concat_arrow a₁ a₂ q₁ q₂:
a₁ ≠ a₂ →
‵[| (a₁, q₁)|] ⊗ ‵[| (a₂, q₂) |] ⇒ ‵{|‵[| (a₁, q₁)|] ⊕ ‵[| (a₂, q₂)|]|}.
Lemma tmerge_with_concat_to_concat_arrow a₁ a₂ q₁ q₂:
a₁ ≠ a₂ →
‵[| (a₁, q₁)|] ⊗ (‵[| (a₁, q₁) |] ⊕ ‵[| (a₂, q₂) |]) ⇒ ‵{|‵[| (a₁, q₁)|] ⊕ ‵[| (a₂, q₂)|]|}.
Lemma tselect_over_nil q : σ⟨ q ⟩(‵{||}) ⇒ ‵{||}.
Lemma tselect_and_comm_arrow (q q₁ q₂:cnraenv) :
σ⟨ q₁ ∧ q₂ ⟩(q) ⇒ σ⟨ q₂ ∧ q₁ ⟩(q).
Lemma tselect_and_comm {τc τenv τin τ} (q ql qr: m ⊧ τin ⇝ Coll τ ⊣ τc;τenv)
(q₁ q₂: m ⊧ τ ⇝ Bool ⊣ τc;τenv) :
(`ql = σ⟨ `q₂ ∧ `q₁ ⟩(`q)) →
(`qr = σ⟨ `q₁ ∧ `q₂ ⟩(`q)) →
ql ≡τ qr.
Lemma tselect_and_arrow (q q₁ q₂:cnraenv) :
σ⟨ q₁ ⟩(σ⟨ q₂ ⟩(q)) ⇒ σ⟨ q₂ ∧ q₁ ⟩(q).
Lemma selection_split_and (q q₁ q₂:cnraenv) :
σ⟨ q₂ ∧ q₁ ⟩(q) ⇒ σ⟨ q₁ ⟩(σ⟨ q₂ ⟩(q)).
Lemma tselect_and {τc τenv τin τ} (q ql qr: m ⊧ τin ⇝ (Coll τ) ⊣ τc;τenv) (q₁ q₂:m ⊧ τ ⇝ Bool ⊣ τc;τenv) :
(`ql = σ⟨ `q₁ ⟩(σ⟨ `q₂ ⟩(`q))) →
(`qr = σ⟨ `q₂ ∧ `q₁ ⟩(`q)) →
(ql ≡τ qr).
Lemma tselect_comm_arrow (q q₁ q₂:cnraenv) :
σ⟨ q₁ ⟩(σ⟨ q₂ ⟩( q )) ⇒ σ⟨ q₂ ⟩(σ⟨ q₁ ⟩( q )).
Lemma tselect_comm {τc τenv τin τ} (q₁ q₂:m ⊧ τ ⇝ Bool ⊣ τc;τenv) (q ql qr: m ⊧ τin ⇝ (Coll τ) ⊣ τc;τenv) :
(`ql = σ⟨ `q₁ ⟩(σ⟨ `q₂ ⟩(`q))) →
(`qr = σ⟨ `q₂ ⟩(σ⟨ `q₁ ⟩(`q))) →
ql ≡τ qr.
Lemma tenvflatten_coll {τc τenv τin τout} (q:m ⊧ τin ⇝ Coll τout ⊣ τc;τenv) (ql qr:m ⊧ τin ⇝ Coll τout ⊣ τc;τenv):
(`ql = ♯flatten(‵{| `q |})) → (`qr = `q) → ql ≡τ qr.
Lemma tenvflatten_coll_arrow (q:cnraenv):
♯flatten(‵{| q |}) ⇒ q.
Lemma tenvflatten_nil_arrow :
♯flatten(‵{||}) ⇒ ‵{||}.
Lemma tenvflatten_map_coll_arrow q₁ q₂ :
♯flatten(χ⟨ ‵{| q₁ |} ⟩( q₂ )) ⇒ χ⟨ q₁ ⟩( q₂ ).
Lemma tflatten_flatten_map_either_nil p₁ p₂ p₃ :
♯flatten( ♯flatten(χ⟨ANEither p₁ ‵{||} ◯ p₂⟩(p₃))) ⇒
♯flatten( χ⟨ANEither( ♯flatten(p₁)) ‵{||} ◯ p₂⟩(p₃)).
Lemma tflatten_mapenv_coll_arrow q₁:
♯flatten(ANMapEnv (‵{| q₁ |})) ⇒ ANMapEnv q₁.
Lemma tdouble_flatten_map_coll_arrow q₁ q₂ q₃ :
♯flatten(χ⟨ χ⟨ ‵{| q₃ |} ⟩( q₁ ) ⟩( q₂ )) ⇒ χ⟨ ‵{| q₃ |} ⟩(♯flatten(χ⟨ q₁ ⟩( q₂ ))).
Lemma tnested_map_over_singletons_arrow q₁ q₂ q₃:
♯flatten(χ⟨ σ⟨ q₁ ⟩(‵{|q₂|}) ⟩(q₃)) ⇒ σ⟨ q₁ ⟩(χ⟨ q₂ ⟩(q₃)).
Lemma tflatten_over_double_map_with_either_arrow q₁ q₂ q₃ q₄ :
♯flatten(χ⟨ χ⟨ q₁ ⟩( σ⟨ q₂ ⟩( (ANEither (‵{|ID|}) ‵{||}) ◯ q₃ ) ) ⟩( q₄ ))
⇒ χ⟨ q₁ ⟩( σ⟨ q₂ ⟩( ♯flatten( χ⟨ (ANEither (‵{|ID|}) ‵{||}) ◯ q₃ ⟩( q₄ ) ) ) ).
Lemma tflatten_over_double_map_arrow q₁ q₂ q₃ :
♯flatten(χ⟨χ⟨ q₁ ⟩( σ⟨ q₂ ⟩(‵{|ID|}) ) ⟩( q₃ )) ⇒ χ⟨ q₁ ⟩( σ⟨ q₂ ⟩( q₃ ) ).
Lemma tselect_over_flatten p₁ p₂ :
σ⟨p₁⟩(♯flatten(p₂)) ⇒ ♯flatten(χ⟨σ⟨p₁⟩(ID)⟩(p₂)).
Lemma tselect_over_flatten_b p₁ p₂ :
♯flatten(χ⟨σ⟨p₁⟩(ID)⟩(p₂)) ⇒ σ⟨p₁⟩(♯flatten(p₂)).
Lemma tmap_over_flatten p₁ p₂ :
χ⟨p₁⟩(♯flatten(p₂)) ⇒ ♯flatten(χ⟨χ⟨p₁⟩(ID)⟩(p₂)).
Lemma tmap_over_flatten_b p₁ p₂ :
♯flatten(χ⟨χ⟨p₁⟩(ID)⟩(p₂)) ⇒ χ⟨p₁⟩(♯flatten(p₂)).
Lemma tselect_over_either p₁ p₂ p₃ :
σ⟨p₁⟩( ANEither p₂ p₃) ⇒ ANEither (σ⟨p₁⟩(p₂)) (σ⟨p₁⟩(p₃)).
Lemma tmap_over_nil q : χ⟨ q ⟩(‵{||}) ⇒ ‵{||}.
Lemma tenvmap_into_id_arrow q :
χ⟨ ID ⟩( q ) ⇒ q.
Lemma tenvmap_map_compose_arrow q₁ q₂ q:
χ⟨ q₁ ⟩( χ⟨ q₂ ⟩( q ) ) ⇒ χ⟨ q₁ ◯ q₂ ⟩( q ).
Lemma tenvmap_singleton_arrow q₁ q₂:
χ⟨ q₁ ⟩( ‵{| q₂ |} ) ⇒ ‵{| q₁ ◯ q₂ |}.
Lemma tmap_full_over_select_arrow q q₁ q₂:
χ⟨ q₂ ⟩(σ⟨ q₁ ⟩(‵{| q |})) ⇒ χ⟨ q₂ ◯ q ⟩(σ⟨ q₁ ◯ q ⟩(‵{| ID |})).
Lemma tmap_over_map_split p₁ p₂ p₃ :
χ⟨χ⟨p₁ ⟩( p₂) ⟩( p₃) ⇒ χ⟨χ⟨p₁ ⟩( ID) ⟩(χ⟨p₂⟩(p₃)).
Lemma tflip_env6_arrow q₁ q₂:
χ⟨ ENV ⊗ ID ⟩(σ⟨ q₁ ⟩(ENV ⊗ q₂)) ⇒ χ⟨ ‵{|ID|} ⟩(σ⟨ q₁ ⟩(ENV ⊗ q₂)).
Lemma tmap_over_either p₁ p₂ p₃ :
χ⟨p₁⟩( ANEither p₂ p₃) ⇒ ANEither (χ⟨p₁⟩(p₂)) (χ⟨p₁⟩(p₃)).
Lemma tmap_over_either_app p₁ p₂ p₃ p₄:
χ⟨p₁⟩( ANEither p₂ p₃ ◯ p₄) ⇒ ANEither (χ⟨p₁⟩(p₂)) (χ⟨p₁⟩(p₃)) ◯ p₄.
Lemma tapp_over_const_arrow d q:
(ANConst d) ◯ q ⇒ (ANConst d).
Lemma tapp_over_env_arrow q :
ENV ◯ q ⇒ ENV.
Lemma tapp_over_id_r_arrow q:
q ◯ ID ⇒ q.
Lemma tapp_over_id_l_arrow q:
ID ◯ q ⇒ q.
Lemma tapp_over_unop_arrow u q₁ q₂:
(ANUnop u q₁) ◯ q₂ ⇒ (ANUnop u (q₁ ◯ q₂)).
Lemma tapp_over_binop_arrow b q q₁ q₂:
(ANBinop b q₂ q₁) ◯ q ⇒ (ANBinop b (q₂ ◯ q) (q₁ ◯ q)).
Lemma tapp_over_map_arrow q q₁ q₂:
(χ⟨q₁⟩(q₂)) ◯ q ⇒ χ⟨ q₁ ⟩(q₂ ◯ q).
Lemma tapp_over_mapconcat_arrow q q₁ q₂:
⋈ᵈ⟨ q₁ ⟩( q₂ ) ◯ q ⇒ ⋈ᵈ⟨ q₁ ⟩( q₂ ◯ q ).
Lemma tapp_over_product_arrow q q₁ q₂:
(q₁ × q₂) ◯ q ⇒ (q₁ ◯ q) × (q₂ ◯ q).
Lemma tapp_over_select_arrow q q₁ q₂:
(σ⟨ q₁ ⟩( q₂ )) ◯ q ⇒ (σ⟨ q₁ ⟩( q₂ ◯ q )).
Lemma tapp_over_select_back_arrow q q₁ q₂:
(σ⟨ q₁ ⟩( q₂ ◯ q )) ⇒ (σ⟨ q₁ ⟩( q₂ )) ◯ q.
Lemma tapp_over_app_arrow q₁ q₂ q₃:
(q₁ ◯ q₂) ◯ q₃ ⇒ q₁ ◯ (q₂ ◯ q₃).
Lemma tselect_over_app_either p₁ p₂ p₃ p₄ :
σ⟨p₁⟩( ANEither p₂ p₃ ◯ p₄ ) ⇒ ANEither (σ⟨p₁⟩(p₂)) (σ⟨p₁⟩(p₃)) ◯ p₄.
Lemma tappenv_over_const_arrow d q:
(ANConst d) ◯ₑ q ⇒ (ANConst d).
Lemma tappenv_over_id_l_arrow q:
ID ◯ₑ q ⇒ ID.
Lemma tapp_over_ignoreid_arrow q₁ q₂:
cnraenv_ignores_id q₁ → q₁ ◯ q₂ ⇒ q₁.
Lemma tappenv_over_env_l_arrow q:
ENV ◯ₑ q ⇒ q.
Lemma tappenv_over_env_r_arrow q:
q ◯ₑ ENV ⇒ q.
Lemma tappenv_over_unop_arrow u q₁ q₂:
(ANUnop u q₁) ◯ₑ q₂ ⇒ (ANUnop u (q₁ ◯ₑ q₂)).
Lemma tunop_over_either u p₁ p₂ :
ANUnop u (ANEither p₁ p₂) ⇒ ANEither (ANUnop u p₁)(ANUnop u p₂).
Lemma tunop_over_either_app u p₁ p₂ p₃:
ANUnop u (ANEither p₁ p₂ ◯ p₃) ⇒ ANEither (ANUnop u p₁)(ANUnop u p₂) ◯ p₃.
Lemma tappenv_over_binop b q₁ q₂ q :
(ANBinop b q₁ q₂) ◯ₑ q ⇒ (ANBinop b (q₁ ◯ₑ q) (q₂ ◯ₑ q)).
Lemma tappenv_over_map_arrow q q₁ q₂:
cnraenv_ignores_id q →
χ⟨ q₁ ⟩( q₂ ) ◯ₑ q ⇒ χ⟨ q₁ ◯ₑ q ⟩( q₂ ◯ₑ q ).
Lemma tappenv_over_map_cnraenv_ignores_env_arrow q₁ q₂:
cnraenv_ignores_env q₁ →
χ⟨ q₁ ⟩( q₂ ) ◯ₑ ANID ⇒ χ⟨ q₁ ◯ₑ ANID ⟩( q₂ ◯ₑ ANID ).
Lemma tappenv_over_select_arrow q q₁ q₂:
cnraenv_ignores_id q →
σ⟨ q₁ ⟩( q₂ ) ◯ₑ q ⇒ σ⟨ q₁ ◯ₑ q ⟩( q₂ ◯ₑ q ).
Lemma tappenv_over_appenv_arrow q q₁ q₂:
(q₁ ◯ₑ q₂) ◯ₑ q ⇒ q₁ ◯ₑ (q₂ ◯ₑ q).
Lemma tappenv_over_app_arrow q q₁ q₂:
cnraenv_ignores_id q → (q₁ ◯ q₂) ◯ₑ q ⇒ (q₁ ◯ₑ q) ◯ (q₂ ◯ₑ q).
Lemma tappenv_over_app_ie_arrow p1 p2 p3:
cnraenv_ignores_env p3 →
((p3 ◯ p2) ◯ₑ p1) ⇒ p3 ◯ (p2 ◯ₑ p1).
Lemma tapp_over_appenv_arrow q q₁ q₂:
cnraenv_ignores_id q₁ → (q₁ ◯ₑ q₂) ◯ q ⇒ q₁ ◯ₑ (q₂ ◯ q).
Lemma tappenv_over_ignoreenv_arrow q₁ q₂:
cnraenv_ignores_env q₁ → q₁ ◯ₑ q₂ ⇒ q₁.
Lemma tappenv_over_env_merge_l_arrow q₁ q:
cnraenv_ignores_env q₁ →
ANAppEnv (ENV ⊗ q₁) q ⇒ q ⊗ q₁.
Lemma tflip_env1_arrow q :
(χ⟨ ENV ⟩(σ⟨ q ⟩(‵{|ID|}))) ◯ₑ ID ⇒ σ⟨ q ⟩(‵{|ID|}) ◯ₑ ID.
Lemma tflip_env4_arrow q₁ q₂:
cnraenv_ignores_env q₁ → (χ⟨ENV⟩( σ⟨ q₁ ⟩(‵{|ID|}))) ◯ₑ q₂ ⇒ χ⟨q₂⟩( σ⟨ q₁ ⟩(‵{|ID|})).
Lemma tflip_env2_arrow q :
σ⟨ q ⟩(‵{|ID|}) ◯ₑ ID ⇒ σ⟨ q ◯ₑ ID ⟩(‵{|ID|}).
Lemma tflatten_through_appenv_arrow q₁ q₂ :
♯flatten(q₁ ◯ₑ q₂) ⇒ ♯flatten(q₁) ◯ₑ q₂.
Lemma tappenv_through_either q₁ q₂ q₃:
cnraenv_ignores_id q₃ →
ANEither q₁ q₂ ◯ₑ q₃ ⇒ ANEither (q₁ ◯ₑ q₃) (q₂ ◯ₑ q₃).
Lemma tmapenv_to_env_arrow q :
(ANMapEnv (ENV)) ◯ q ⇒ ENV.
Lemma tmapenv_over_singleton_arrow q₁ q₂ :
(ANMapEnv q₁) ◯ₑ (‵{|q₂|}) ⇒ ‵{| q₁ ◯ₑ q₂ |}.
Lemma tmapenv_to_map_arrow q₁ q₂:
cnraenv_ignores_id q₁ →
(ANMapEnv q₁) ◯ₑ q₂ ⇒ χ⟨ q₁ ◯ₑ ID ⟩(q₂).
Lemma tcompose_selects_in_mapenv_arrow q₁ q₂ :
(♯flatten(ANMapEnv (χ⟨ENV⟩(σ⟨ q₁ ⟩( ‵{| ID |}))))) ◯ₑ (χ⟨ENV⟩(σ⟨ q₂ ⟩( ‵{| ID |})))
⇒ (χ⟨ENV⟩(σ⟨ q₁ ⟩(σ⟨ q₂ ⟩( ‵{| ID |})))).
Lemma tappenv_mapenv_to_map_arrow q a:
ANAppEnv (ANMapEnv q) (ENV ⊗ ‵[| (a, ID)|]) ⇒
χ⟨(q ◯ (ANUnop (ADot a) ANEnv)) ◯ₑ ID⟩( (ENV ⊗ ‵[| (a, ID)|]) ).
Lemma tappenv_flatten_mapenv_to_map_arrow q a:
ANAppEnv (♯flatten(ANMapEnv q)) (ENV ⊗ ‵[| (a, ID)|]) ⇒
♯flatten(χ⟨(q ◯ (ANUnop (ADot a) ANEnv)) ◯ₑ ID⟩( (ENV ⊗ ‵[| (a, ID)|]) )).
Lemma ttostring_dstring_arrow s:
(ANUnop AToString (ANConst (dstring s))) ⇒ (ANConst (dstring s)).
Lemma ttostring_tostring_arrow q:
(ANUnop AToString (ANUnop AToString q)) ⇒ (ANUnop AToString q).
Lemma ttostring_sconcat_arrow q₁ q₂:
(ANUnop AToString (ANBinop ASConcat q₁ q₂)) ⇒ (ANBinop ASConcat q₁ q₂).
Lemma trproject_nil p :
π[nil](p) ⇒ ‵[||].
Lemma trproject_over_concat_rec_r_in sl s p₁ p₂ :
In s sl →
π[sl](p₁ ⊕ ‵[| (s, p₂) |]) ⇒ π[remove string_dec s sl](p₁) ⊕ ‵[| (s, p₂) |] .
Lemma trproject_over_const sl l :
π[sl](ANConst (drec l)) ⇒ ANConst (drec (rproject l sl)).
Lemma trproject_over_rec_in sl s p :
In s sl →
π[sl](‵[| (s, p) |]) ⇒ ‵[| (s, p) |].
Lemma trproject_over_rec_nin sl s p :
¬ In s sl →
π[sl](‵[| (s, p) |]) ⇒ ‵[||].
Lemma trproject_over_concat_rec_r_nin sl s p₁ p₂ :
¬ In s sl →
π[sl](p₁ ⊕ ‵[| (s, p₂) |]) ⇒ π[sl](p₁).
Lemma trproject_over_concat_rec_l_nin sl s p₁ p₂ :
¬ In s sl →
π[sl](‵[| (s, p₁) |] ⊕ p₂) ⇒ π[sl](p₂).
Lemma trproject_over_concat_recs_in_in sl s₁ p₁ s₂ p₂ :
In s₁ sl → In s₂ sl →
π[sl](‵[| (s₁, p₁) |] ⊕ ‵[| (s₂, p₂) |]) ⇒ ‵[| (s₁, p₁) |] ⊕ ‵[| (s₂, p₂) |].
Lemma trproject_over_rproject sl1 sl2 p :
π[sl1](π[sl2](p)) ⇒ π[set_inter string_dec sl2 sl1](p).
Lemma trproject_over_either sl p1 p2 :
π[sl](ANEither p1 p2) ⇒ ANEither (π[sl](p1)) (π[sl](p2)).
Lemma tcount_over_map p₁ p₂ :
♯count(χ⟨p₁⟩(p₂)) ⇒ ♯count(p₂).
Lemma tcount_over_flat_map_map p₁ p₂ p₃ :
♯count(♯flatten(χ⟨χ⟨p₁⟩(p₂)⟩(p₃))) ⇒
♯count(♯flatten(χ⟨p₂⟩(p₃))).
Lemma tmap_over_either_nil_b p₁ p₂ :
ANEither (χ⟨p₁⟩(p₂)) ‵{||} ⇒ χ⟨p₁⟩(ANEither p₂ ‵{||}).
Lemma tcount_over_flat_map_either_nil_map p₁ p₂ p₃ :
♯count(♯flatten(χ⟨ANEither (χ⟨p₁⟩(p₂)) ‵{||}⟩(p₃))) ⇒
♯count(♯flatten(χ⟨ANEither p₂ ‵{||}⟩(p₃))).
Lemma tcount_over_flat_map_either_nil_app_map p₁ p₂ p₃ p₄:
♯count(♯flatten(χ⟨ANEither (χ⟨p₁⟩(p₂)) ‵{||} ◯ p₄⟩(p₃))) ⇒
♯count(♯flatten(χ⟨ANEither p₂ ‵{||} ◯ p₄⟩(p₃))).
Lemma tcount_over_flat_map_either_nil_app_singleton p₁ p₂ p₃:
♯count(♯flatten(χ⟨ANEither (‵{| p₁ |}) ‵{||} ◯ p₃⟩(p₂))) ⇒
♯count(♯flatten(χ⟨ANEither (‵{| ANConst dunit |}) ‵{||} ◯ p₃⟩(p₂))).
Lemma tmapconcat_over_singleton p₁ :
⋈ᵈ⟨ p₁ ⟩(‵{| ‵[||] |}) ⇒ p₁ ◯ (‵[||]).
composite lemmas: these are just composites of previous rewrites.
They are here since the optimizer uses them.