blob: 775b633384b6f9b40eaa1349abfda2a0dc88275f (
plain)
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
|
(set-info :smt-lib-version 2.6)
(set-logic UFDT)
(set-info :status unsat)
(declare-sort A$ 0)
(declare-sort Nat$ 0)
(declare-sort Nat_nat_fun$ 0)
(declare-sort Enat_nat_fun$ 0)
(declare-sort Nat_bool_fun$ 0)
(declare-sort Nat_enat_fun$ 0)
(declare-sort Bool_bool_fun$ 0)
(declare-sort Enat_bool_fun$ 0)
(declare-sort Enat_enat_fun$ 0)
(declare-sort A_stream_bool_fun$ 0)
(declare-sort Nat_bool_fun_nat_fun$ 0)
(declare-sort Nat_nat_bool_fun_fun$ 0)
(declare-sort Bool_enat_bool_fun_fun$ 0)
(declare-sort Enat_enat_bool_fun_fun$ 0)
(declare-sort Nat_bool_fun_nat_bool_fun_fun$ 0)
(declare-datatypes ((Nat_option$ 0)(Enat$ 0)) (((none$) (some$ (the$ Nat$)))
((abs_enat$ (rep_enat$ Nat_option$)))
))
(declare-sort A_stream$ 0)
(declare-fun shd$ (A_stream$) A$)
(declare-fun stl$ (A_stream$) A_stream$)
(declare-fun sCons$ (A$ A_stream$) A_stream$)
(declare-fun i$ () Nat$)
(declare-fun p$ () A_stream_bool_fun$)
(declare-fun ia$ () Nat$)
(declare-fun uu$ (Nat$) Nat_bool_fun$)
(declare-fun suc$ (Nat$) Nat$)
(declare-fun uua$ (Enat$) Nat_bool_fun$)
(declare-fun uub$ (Bool_bool_fun$) Nat_bool_fun_nat_bool_fun_fun$)
(declare-fun uuc$ (Enat$) Nat_bool_fun$)
(declare-fun uud$ () Nat_nat_fun$)
(declare-fun eSuc$ (Enat$) Enat$)
(declare-fun enat$ (Nat$) Enat$)
(declare-fun less$ (Nat$) Nat_bool_fun$)
(declare-fun plus$ (Enat$) Enat_enat_fun$)
(declare-fun less$a (Enat$) Enat_bool_fun$)
(declare-fun omega$ () A_stream$)
(declare-fun plus$a (Nat$) Nat_nat_fun$)
(declare-fun sdrop$ (Nat$ A_stream$) A_stream$)
(declare-fun omega$a () A_stream$)
(declare-fun sfirst$ (A_stream_bool_fun$ A_stream$) Enat$)
(declare-fun fun_app$ (Nat_bool_fun$ Nat$) Bool)
(declare-fun less_eq$ (Nat$) Nat_bool_fun$)
(declare-fun case_nat$ (Bool) Nat_bool_fun_nat_bool_fun_fun$)
(declare-fun fun_app$a (Enat_bool_fun$ Enat$) Bool)
(declare-fun fun_app$b (Bool_enat_bool_fun_fun$ Bool) Enat_bool_fun$)
(declare-fun fun_app$c (Nat_bool_fun_nat_bool_fun_fun$ Nat_bool_fun$) Nat_bool_fun$)
(declare-fun fun_app$d (Bool_bool_fun$ Bool) Bool)
(declare-fun fun_app$e (Nat_nat_fun$ Nat$) Nat$)
(declare-fun fun_app$f (A_stream_bool_fun$ A_stream$) Bool)
(declare-fun fun_app$g (Nat_enat_fun$ Nat$) Enat$)
(declare-fun fun_app$h (Enat_enat_fun$ Enat$) Enat$)
(declare-fun fun_app$i (Enat_nat_fun$ Enat$) Nat$)
(declare-fun fun_app$j (Enat_enat_bool_fun_fun$ Enat$) Enat_bool_fun$)
(declare-fun fun_app$k (Nat_nat_bool_fun_fun$ Nat$) Nat_bool_fun$)
(declare-fun fun_app$l (Nat_bool_fun_nat_fun$ Nat_bool_fun$) Nat$)
(declare-fun greatest$ (Enat_bool_fun$) Enat$)
(declare-fun less_eq$a (Enat$) Enat_bool_fun$)
(declare-fun rec_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$)
(declare-fun case_enat$ (Nat_bool_fun$) Bool_enat_bool_fun_fun$)
(declare-fun greatest$a () Nat_bool_fun_nat_fun$)
(declare-fun greatestM$ (Nat_nat_fun$) Nat_bool_fun_nat_fun$)
(assert (and
(forall ((?v0 Nat$) (?v1 A_stream_bool_fun$) (?v2 A_stream$)) (=> (fun_app$a (less$a (enat$ ?v0)) (sfirst$ ?v1 ?v2)) (not (fun_app$f ?v1 (sdrop$ ?v0 ?v2)))) )
(not (fun_app$a (less_eq$a (sfirst$ p$ omega$)) (enat$ (suc$ ia$))))
(fun_app$f p$ (sdrop$ (suc$ ia$) omega$))
(forall ((?v0 Enat$) (?v1 Enat$)) (=> (not (fun_app$a (less$a ?v0) ?v1)) (fun_app$a (less_eq$a ?v1) ?v0)) )
))
(check-sat)
(exit)
|
