-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPartialRefinement.prf
115 lines (114 loc) · 4.38 KB
/
PartialRefinement.prf
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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
(PartialRefinement
(strongPartCaseWeak 0
(strongPartCaseWeak-1 nil 3655109962
("" (skolem 1 (pl1 pl2 m))
(("" (bddsimp)
(("1" (expand* strongPartialRefinement weakPartialRefinement)
(("1" (bddsimp)
(("1" (skolem 1 c)
(("1" (inst -3 c)
(("1" (expand identity?)
(("1" (inst -1 c)
(("1" (replace -1 1) (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (typepred m)
(("2" (expand subset?)
(("2" (skolem 1 c)
(("2" (inst -3 c)
(("2" (expand member)
(("2" (bddsimp)
(("2" (expand image)
(("2" (expand domain)
(("2" (skolem -6 l)
(("2" (expand identity?)
(("2"
(inst -3 l)
(("2"
(lemma
"maps[Conf,Conf].getRightResult")
(("2"
(inst -1 m c l)
(("2"
(bddsimp)
(("2"
(replace -2 -5)
(("2"
(replace -5 -1)
(("2"
(inst 1 l)
(("2"
(replace -5 1)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* weakPartialRefinement strongPartialRefinement)
(("2" (bddsimp)
(("2" (skolem 1 c)
(("2" (inst -4 c)
(("2" (expand identity?)
(("2" (inst -1 c)
(("2" (replace -1 -4) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Conf formal-type-decl nil PartialRefinement nil)
(identity? const-decl "bool" maps_identity nil)
(getRightResult formula-decl nil maps nil)
(dom const-decl "set[S]" maps nil)
(image const-decl "finite_sets[T].finite_set" maps nil)
(member const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(unique const-decl "bool" maps nil)
(FM formal-type-decl nil PartialRefinement nil)
({\|\|} formal-const-decl "[FM -> set[Conf]]" PartialRefinement
nil)
(Asset formal-type-decl nil PartialRefinement nil)
(AssetName formal-type-decl nil PartialRefinement nil)
(CK formal-type-decl nil PartialRefinement nil)
(mapping type-eq-decl nil maps nil)
([\|\|] formal-const-decl
"[CK -> [mapping -> [Conf -> finite_sets[Asset].finite_set]]]"
PartialRefinement nil)
(CM type-eq-decl nil PartialRefinementWeak nil)
(subset? const-decl "bool" sets nil)
(domain const-decl "finite_sets[S].finite_set" maps nil)
(AM type-eq-decl nil SPLrefinement nil)
(ArbitrarySPL type-eq-decl nil SPLrefinement nil)
(wfPL const-decl "bool" SPLrefinement nil)
(PL type-eq-decl nil SPLrefinement nil)
(strongPartialRefinement const-decl "bool"
PartialRefinementStrong nil)
(weakPartialRefinement const-decl "bool" PartialRefinementWeak
nil))
shostak)))