equal
deleted
inserted
replaced
23 |
23 |
24 drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)" |
24 drop_map :: "[nat, (nat=>'b) * 'c] => 'b * ((nat=>'b) * 'c)" |
25 "drop_map i == %(g, uu). (g i, (delete_map i g, uu))" |
25 "drop_map i == %(g, uu). (g i, (delete_map i g, uu))" |
26 |
26 |
27 lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set" |
27 lift_set :: "[nat, ('b * ((nat=>'b) * 'c)) set] => ((nat=>'b) * 'c) set" |
28 "lift_set i A == lift_map i `` A" |
28 "lift_set i A == lift_map i ` A" |
29 |
29 |
30 lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program" |
30 lift :: "[nat, ('b * ((nat=>'b) * 'c)) program] => ((nat=>'b) * 'c) program" |
31 "lift i == rename (lift_map i)" |
31 "lift i == rename (lift_map i)" |
32 |
32 |
33 (*simplifies the expression of specifications*) |
33 (*simplifies the expression of specifications*) |