(* Advanced properties ******************************************************)
lemma cpmuwe_abbr_neg (h) (n) (G) (L) (T):
- â\88\80V,U. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] -â\93\93V.U â\86\92 â¦\83G,Lâ¦\84 ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U.
+ â\88\80V,U. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] -â\93\93V.U â\86\92 â\9d¨G,Lâ\9d© ⊢ T ➡*𝐍𝐖*[h,n] -ⓓV.U.
/3 width=5 by cnuw_abbr_neg, cpmuwe_intro/ qed.
lemma cpmuwe_abst (h) (n) (p) (G) (L) (T):
- â\88\80W,U. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W.U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*ð\9d\90\8dð\9d\90\96*[h,n] â\93\9b{p}W.U.
+ â\88\80W,U. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] â\93\9b[p]W.U â\86\92 â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*ð\9d\90\8dð\9d\90\96*[h,n] â\93\9b[p]W.U.
/3 width=5 by cnuw_abst, cpmuwe_intro/ qed.