Changeset 3510


Ignore:
Timestamp:
Sep 26, 2014, 6:34:39 PM (5 years ago)
Author:
sacerdot
Message:

One proof closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Final.ma

    r3509 r3510  
    9494    #lbl' #pc * #Hmem #EQ destruct
    9595    >(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'
     99cases (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 ⊢ (??%?); % | // ]
     104qed. 
    98105cases daemon
    99106qed.
Note: See TracChangeset for help on using the changeset viewer.