forked from kframework/javascript-semantics
-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathfloat_set.k
More file actions
47 lines (42 loc) · 2.41 KB
/
Copy pathfloat_set.k
File metadata and controls
47 lines (42 loc) · 2.41 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
module FLOAT-SET
imports FLOAT-HOOKS
syntax FloatSet ::= FloatSet "U" FloatSet [function, left, smtlib(float_set_cup)]
| ".FloatSet" [function, smtlib(float_set_emp)]
| "{" Float "}" [function, smtlib(float_set_ele), klabel(float_set_ele)]
| FloatSet "-FloatSet" FloatSet [function, smtlib(float_set_dif)]
syntax Bool ::= Float "inFloatSet" FloatSet [function, smtlib(float_set_mem)]
| FloatSet "<FloatSet" FloatSet [function, smtlib(float_set_lt)]
| FloatSet "<=FloatSet" FloatSet [function, smtlib(float_set_le)]
rule S:FloatSet U .FloatSet => S [lemma]
rule .FloatSet U S:FloatSet => S [lemma]
rule I:Float inFloatSet (S1:FloatSet U S2:FloatSet)
=> (I inFloatSet S1) orBool (I inFloatSet S2)
[lemma]
rule _:Float inFloatSet .FloatSet => false [lemma]
rule I1:Float inFloatSet { I2:Float } => I1 ==K I2 [lemma]
rule S:FloatSet <FloatSet (S1:FloatSet U S2:FloatSet)
=> (S:FloatSet <FloatSet S1:FloatSet) andBool (S:FloatSet <FloatSet S2:FloatSet)
[lemma]
rule (S1:FloatSet U S2:FloatSet) <FloatSet S:FloatSet
=> (S1:FloatSet <FloatSet S:FloatSet) andBool (S2:FloatSet <FloatSet S:FloatSet)
[lemma]
rule _:FloatSet <FloatSet .FloatSet => true [lemma]
rule .FloatSet <FloatSet _:FloatSet => true [lemma]
rule { I1:Float } <FloatSet { I2:Float } => I1 <Float I2 [lemma]
rule S:FloatSet <=FloatSet (S1:FloatSet U S2:FloatSet)
=> (S:FloatSet <=FloatSet S1:FloatSet) andBool (S:FloatSet <=FloatSet S2:FloatSet)
[lemma]
rule (S1:FloatSet U S2:FloatSet) <=FloatSet S:FloatSet
=> (S1:FloatSet <=FloatSet S:FloatSet) andBool (S2:FloatSet <=FloatSet S:FloatSet)
[lemma]
rule _:FloatSet <=FloatSet .FloatSet => true [lemma]
rule .FloatSet <=FloatSet _:FloatSet => true [lemma]
rule { I1:Float } <=FloatSet { I2:Float } => I1 <=Float I2 [lemma]
rule S:FloatSet -FloatSet (S1:FloatSet U S2:FloatSet)
=> (S:FloatSet -FloatSet S1:FloatSet) U (S:FloatSet -FloatSet S2:FloatSet)
[lemma]
rule (S1:FloatSet U S2:FloatSet) -FloatSet S:FloatSet
=> (S1:FloatSet -FloatSet S:FloatSet) U (S2:FloatSet -FloatSet S:FloatSet)
[lemma]
rule .FloatSet -FloatSet _:FloatSet => .FloatSet [lemma]
endmodule