25 |
25 |
26 defs |
26 defs |
27 |
27 |
28 |
28 |
29 ProjA_def |
29 ProjA_def |
30 "ProjA ex == (fst (fst ex), ProjA2`(snd ex))" |
30 "ProjA ex == (fst (fst ex), ProjA2$(snd ex))" |
31 |
31 |
32 ProjB_def |
32 ProjB_def |
33 "ProjB ex == (snd (fst ex), ProjB2`(snd ex))" |
33 "ProjB ex == (snd (fst ex), ProjB2$(snd ex))" |
34 |
34 |
35 |
35 |
36 ProjA2_def |
36 ProjA2_def |
37 "ProjA2 == Map (%x.(fst x,fst(snd x)))" |
37 "ProjA2 == Map (%x.(fst x,fst(snd x)))" |
38 |
38 |
39 ProjB2_def |
39 ProjB2_def |
40 "ProjB2 == Map (%x.(fst x,snd(snd x)))" |
40 "ProjB2 == Map (%x.(fst x,snd(snd x)))" |
41 |
41 |
42 |
42 |
43 Filter_ex_def |
43 Filter_ex_def |
44 "Filter_ex sig ex == (fst ex,Filter_ex2 sig`(snd ex))" |
44 "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))" |
45 |
45 |
46 |
46 |
47 Filter_ex2_def |
47 Filter_ex2_def |
48 "Filter_ex2 sig == Filter (%x. fst x:actions sig)" |
48 "Filter_ex2 sig == Filter (%x. fst x:actions sig)" |
49 |
49 |
50 stutter_def |
50 stutter_def |
51 "stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)" |
51 "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)" |
52 |
52 |
53 stutter2_def |
53 stutter2_def |
54 "stutter2 sig ==(fix`(LAM h ex. (%s. case ex of |
54 "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of |
55 nil => TT |
55 nil => TT |
56 | x##xs => (flift1 |
56 | x##xs => (flift1 |
57 (%p.(If Def ((fst p)~:actions sig) |
57 (%p.(If Def ((fst p)~:actions sig) |
58 then Def (s=(snd p)) |
58 then Def (s=(snd p)) |
59 else TT fi) |
59 else TT fi) |
60 andalso (h`xs) (snd p)) |
60 andalso (h$xs) (snd p)) |
61 `x) |
61 $x) |
62 )))" |
62 )))" |
63 |
63 |
64 par_execs_def |
64 par_execs_def |
65 "par_execs ExecsA ExecsB == |
65 "par_execs ExecsA ExecsB == |
66 let exA = fst ExecsA; sigA = snd ExecsA; |
66 let exA = fst ExecsA; sigA = snd ExecsA; |