48 "_Enabled" :: lift => lift ("(Enabled _)" [100] 100) |
48 "_Enabled" :: lift => lift ("(Enabled _)" [100] 100) |
49 |
49 |
50 translations |
50 translations |
51 "ACT A" => "(A::state*state => _)" |
51 "ACT A" => "(A::state*state => _)" |
52 "_before" == "before" |
52 "_before" == "before" |
53 "_after" => "_prime" |
53 "_after" == "after" |
|
54 "_prime" => "_after" |
54 "_unchanged" == "unch" |
55 "_unchanged" == "unch" |
55 "_prime" == "after" |
|
56 "_SqAct" == "SqAct" |
56 "_SqAct" == "SqAct" |
57 "_AnAct" == "AnAct" |
57 "_AnAct" == "AnAct" |
58 "_Enabled" == "enabled" |
58 "_Enabled" == "enabled" |
59 "w |= [A]_v" <= "_SqAct A v w" |
59 "w |= [A]_v" <= "_SqAct A v w" |
60 "w |= <A>_v" <= "_AnAct A v w" |
60 "w |= <A>_v" <= "_AnAct A v w" |
61 "s |= Enabled A" <= "_Enabled A s" |
61 "s |= Enabled A" <= "_Enabled A s" |
62 "w |= unchanged f" <= "_unchanged f w" |
62 "w |= unchanged f" <= "_unchanged f w" |
63 |
63 |
64 rules |
64 rules |
65 unl_before "(ACT $v) (s,t) == v s" |
65 unl_before "(ACT $v) (s,t) == v s" |
66 unl_after "(ACT v`) (s,t) == v t" |
66 unl_after "(ACT v$) (s,t) == v t" |
67 |
67 |
68 unchanged_def "(s,t) |= unchanged v == (v t = v s)" |
68 unchanged_def "(s,t) |= unchanged v == (v t = v s)" |
69 square_def "ACT [A]_v == ACT (A | unchanged v)" |
69 square_def "ACT [A]_v == ACT (A | unchanged v)" |
70 angle_def "ACT <A>_v == ACT (A & ~ unchanged v)" |
70 angle_def "ACT <A>_v == ACT (A & ~ unchanged v)" |
71 |
71 |