X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fbasic_machines.ma;h=a2357682972f1ddd4e67458f16e98de02d191eb2;hb=d5da44537d93ee16e1f440e5ce3fd69b32c3b730;hp=82d4758c250c31eeac7545f6dd89179c2996d52c;hpb=53656d48b302c50e775159dc62e56cd7b1550676;p=helm.git

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 82d4758c2..a23576829 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -197,6 +197,27 @@ lemma test_char_inv :
 #sig #P #f #t #t0 #HPt * #_ //
 qed.
 
+definition test_null ≝ λalpha.test_char alpha (λ_.true).
+
+definition R_test_null_true ≝ λalpha,t1,t2.
+  current alpha t1 ≠ None ? ∧ t1 = t2.
+  
+definition R_test_null_false ≝ λalpha,t1,t2.
+  current alpha t1 = None ? ∧ t1 = t2.
+  
+lemma sem_test_null : ∀alpha.
+  test_null alpha ⊨ [ tc_true : R_test_null_true alpha, R_test_null_false alpha].
+#alpha #t1 cases (sem_test_char alpha (λ_.true) t1) #k * #outc * * #Hloop #Htrue
+#Hfalse %{k} %{outc} % [ %
+[ @Hloop
+| #Houtc cases (Htrue ?) [| @Houtc] * #c * #Hcurt1 #_ #Houtc1 %
+  [ >Hcurt1 % #H destruct (H) | <Houtc1 % ] ]
+| #Houtc cases (Hfalse ?) [| @Houtc] #Habsurd #Houtc %
+  [ cases (current alpha t1) in Habsurd; // #c1 #Habsurd 
+    lapply (Habsurd ? (refl ??)) #H destruct (H)
+  | <Houtc % ] ]
+qed.
+
 (************************************* swap ***********************************)
 definition swap_states : FinSet → FinSet ≝ 
   λalpha:FinSet.FinProd (initN 4) alpha.