Changeset 3510

Timestamp:

Sep 26, 2014, 6:34:39 PM (5 years ago)

Author:

sacerdot

Message:

One proof closed.

File:

• LTS/Final.ma (modified) (1 diff)

LTS/Final.ma

@@ -94 +94 @@
     #lbl' #pc * #Hmem #EQ destruct
     >(proj1 … (static_analisys_ok … EQmap … Hmem))
-    @(proj2 … (static_analisys_ok … EQmap … Hmem))
-]
+    @(proj2 … (static_analisys_ok … EQmap … Hmem))]
+#S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds
+#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
+cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi')
+#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
+%{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
+@(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map
+[2: <EQcostlabs in ⊢ (??%?); % | // ]
+qed.  
 cases daemon
 qed.