52 "p2 n \<Longrightarrow> p2 n" |
52 "p2 n \<Longrightarrow> p2 n" |
53 |
53 |
54 coinductive q2 :: "nat \<Rightarrow> bool" where |
54 coinductive q2 :: "nat \<Rightarrow> bool" where |
55 "q2 n \<Longrightarrow> q2 n" |
55 "q2 n \<Longrightarrow> q2 n" |
56 |
56 |
57 lemma "p2 = {}" |
57 lemma "p2 = bot" |
58 nitpick [expect = none] |
58 nitpick [expect = none] |
59 nitpick [dont_star_linear_preds, expect = none] |
59 nitpick [dont_star_linear_preds, expect = none] |
60 sorry |
60 sorry |
61 |
61 |
62 lemma "q2 = {}" |
62 lemma "q2 = bot" |
63 nitpick [expect = genuine] |
63 nitpick [expect = genuine] |
64 nitpick [dont_star_linear_preds, expect = genuine] |
64 nitpick [dont_star_linear_preds, expect = genuine] |
65 nitpick [wf, expect = quasi_genuine] |
65 nitpick [wf, expect = quasi_genuine] |
66 oops |
66 oops |
67 |
67 |
68 lemma "p2 = UNIV" |
68 lemma "p2 = top" |
69 nitpick [expect = genuine] |
69 nitpick [expect = genuine] |
70 nitpick [dont_star_linear_preds, expect = genuine] |
70 nitpick [dont_star_linear_preds, expect = genuine] |
71 oops |
71 oops |
72 |
72 |
73 lemma "q2 = UNIV" |
73 lemma "q2 = top" |
74 nitpick [expect = none] |
74 nitpick [expect = none] |
75 nitpick [dont_star_linear_preds, expect = none] |
75 nitpick [dont_star_linear_preds, expect = none] |
76 nitpick [wf, expect = quasi_genuine] |
76 nitpick [wf, expect = quasi_genuine] |
77 sorry |
77 sorry |
78 |
78 |
121 lemma "p4 = q4" |
121 lemma "p4 = q4" |
122 nitpick [expect = none] |
122 nitpick [expect = none] |
123 nitpick [non_wf, expect = none] |
123 nitpick [non_wf, expect = none] |
124 sorry |
124 sorry |
125 |
125 |
126 lemma "p3 = UNIV - p4" |
126 lemma "p3 = top - p4" |
127 nitpick [expect = none] |
127 nitpick [expect = none] |
128 nitpick [non_wf, expect = none] |
128 nitpick [non_wf, expect = none] |
129 sorry |
129 sorry |
130 |
130 |
131 lemma "q3 = UNIV - q4" |
131 lemma "q3 = top - q4" |
132 nitpick [expect = none] |
132 nitpick [expect = none] |
133 nitpick [non_wf, expect = none] |
133 nitpick [non_wf, expect = none] |
134 sorry |
134 sorry |
135 |
135 |
136 lemma "p3 \<inter> q4 \<noteq> {}" |
136 lemma "inf p3 q4 \<noteq> bot" |
137 nitpick [expect = potential] |
137 nitpick [expect = potential] |
138 nitpick [non_wf, expect = potential] |
138 nitpick [non_wf, expect = potential] |
139 sorry |
139 sorry |
140 |
140 |
141 lemma "q3 \<inter> p4 \<noteq> {}" |
141 lemma "inf q3 p4 \<noteq> bot" |
142 nitpick [expect = potential] |
142 nitpick [expect = potential] |
143 nitpick [non_wf, expect = potential] |
143 nitpick [non_wf, expect = potential] |
144 sorry |
144 sorry |
145 |
145 |
146 lemma "p3 \<union> q4 \<noteq> UNIV" |
146 lemma "sup p3 q4 \<noteq> top" |
147 nitpick [expect = potential] |
147 nitpick [expect = potential] |
148 nitpick [non_wf, expect = potential] |
148 nitpick [non_wf, expect = potential] |
149 sorry |
149 sorry |
150 |
150 |
151 lemma "q3 \<union> p4 \<noteq> UNIV" |
151 lemma "sup q3 p4 \<noteq> top" |
152 nitpick [expect = potential] |
152 nitpick [expect = potential] |
153 nitpick [non_wf, expect = potential] |
153 nitpick [non_wf, expect = potential] |
154 sorry |
154 sorry |
155 |
155 |
156 end |
156 end |