Changeset 2799


Ignore:
Timestamp:
Mar 7, 2013, 1:04:47 PM (7 years ago)
Author:
tranquil
Message:
  • added taaf_to_taa, conversion from trace_any_any_free to trace_any_any, with a proof obbligation
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2756 r2799  
    182182    taa_step ???? H I J (taa_append_taa … tl taa2)
    183183  ] st3.
     184
     185definition taaf_to_taa : ∀S : abstract_status.∀s1,s2,taaf.
     186if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
     187trace_any_any S s1 s2 ≝
     188λS,s1,s2,taaf.
     189match taaf return λs1,s2,taaf.if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
     190  trace_any_any S s1 s2 with
     191[ taaf_base s ⇒ λ_.taa_base …
     192| taaf_step s1 s2 s3 taa ex cl ⇒ λncost.
     193  taa_append_taa … taa (taa_step … ex cl ncost (taa_base …))
     194| taaf_step_jump s1 s2 s3 taa ex cl cost ⇒ λncost.Ⓧ(absurd … cost ncost)
     195].
    184196
    185197lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
Note: See TracChangeset for help on using the changeset viewer.