Finalized copy sub-machine of the universal turing machine. Some new results

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / dynamic / nta.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
index 7a24249f20013a35ec85b02049575b862e0e20fc..fa4a8ed8f175cb22e8952b7ec3c7807853df1bbf 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
@@ -29,7 +29,7 @@ inductive nta (h:sh): lenv → relation term ≝
             nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
 | nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
             nta h L (ⓐV.T) (ⓐV.U)
-| nta_cast: â\88\80L,T,U. nta h L T U â\86\92 nta h L (â\93£U. T) U
+| nta_cast: â\88\80L,T,U. nta h L T U â\86\92 nta h L (â\93\9dU. T) U
 | nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
             nta h L T U2
 .
@@ -41,11 +41,11 @@ interpretation "native type assignment (term)"
 
 (* Basic_1: was: ty3_cast *)
 lemma nta_cast_old: ∀h,L,W,T,U.
-                    â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U : W â\86\92 â¦\83h, Lâ¦\84 â\8a¢ â\93£U.T : â\93£W.U.
+                    â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â¦\83h, Lâ¦\84 â\8a¢ U : W â\86\92 â¦\83h, Lâ¦\84 â\8a¢ â\93\9dU.T : â\93\9dW.U.
 /4 width=3/ qed.
 
 (* Basic_1: was: ty3_typecheck *)
-lemma nta_typecheck: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\83T0. â¦\83h, Lâ¦\84 â\8a¢ â\93£U.T : T0.
+lemma nta_typecheck: â\88\80h,L,T,U. â¦\83h, Lâ¦\84 â\8a¢ T : U â\86\92 â\88\83T0. â¦\83h, Lâ¦\84 â\8a¢ â\93\9dU.T : T0.
 /3 width=2/ qed.
 
 (* Basic_1: removed theorems 4: