Changeset 3510
- Timestamp:
- Sep 26, 2014, 6:34:39 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Final.ma
r3509 r3510 94 94 #lbl' #pc * #Hmem #EQ destruct 95 95 >(proj1 … (static_analisys_ok … EQmap … Hmem)) 96 @(proj2 … (static_analisys_ok … EQmap … Hmem)) 97 ] 96 @(proj2 … (static_analisys_ok … EQmap … Hmem))] 97 #S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds 98 #R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi' 99 cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi') 100 #sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas' 101 %{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts 102 @(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map 103 [2: <EQcostlabs in ⊢ (??%?); % | // ] 104 qed. 98 105 cases daemon 99 106 qed.
Note: See TracChangeset
for help on using the changeset viewer.