- the theory of delifting substitution is done

[helm.git] / matita / matita / lib / turing / basic_machines.ma

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 1c1ce3020b824d3c37c1bb48f7581c060deec56f..a2357682972f1ddd4e67458f16e98de02d191eb2 100644 (file)
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -192,6 +192,32 @@ lemma sem_test_char :
 ]
 qed.
 
+lemma test_char_inv : 
+  ∀sig.∀P:tape sig → Prop.∀f,t,t0.P t → Rtc_true sig f t t0 → P t0.
+#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.
@@ -297,4 +323,4 @@ lemma sem_swap_l : ∀alpha,foo.
       [#b #rs #H destruct | #a #b #ls #rs #H destruct normalize //
     ]
   ]
-qed.
+qed.
\ No newline at end of file