Ignore:
Timestamp:
Dec 14, 2011, 1:18:30 PM (8 years ago)
Author:
sacerdot
Message:

Porting to last standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1566 r1605  
    719719  (REACTIVE: ∀tr,s1,e1.
    720720    execution_isteps tr s e s1 e1 →
    721     (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
     721    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
    722722  : traceinf' ≝ ?.
    723723lapply (REACTIVE E0 s e (isteps_none …));
     
    739739let corec reactive_traceinf'' ge s e
    740740  (EXEC:exec_from ge s e)
    741   (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
     741  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    742742  (REACTIVE: ∀tr,s1,e1.
    743743    execution_isteps tr s e s1 e1 →
    744     (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
     744    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
    745745  : traceinf' ≝ ?.
    746746cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
     
    771771let corec show_reactive' ge s e
    772772  (EXEC:exec_from ge s e)
    773   (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
     773  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    774774  (REACTIVE: ∀tr1,s1,e1.
    775775    execution_isteps tr1 s e s1 e1 →
    776     (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
     776    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
    777777  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
    778778(*>(unroll_traceinf' (reactive_traceinf'' …)) *)
     
    791791  ∀REACTIVE:∀tr,s1,e1.
    792792    execution_isteps tr s e s1 e1 →
    793     (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)).
     793    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0).
    794794  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
    795795[ #ge #s #e #EXEC #REACTIVE
Note: See TracChangeset for help on using the changeset viewer.