1; COMMAND-LINE: --rewrite-rules 2(set-logic AUFLIRA) 3 4;; DATATYPE 5;; nat = succ(pred : nat) | zero, 6;; list = cons(car : tree, cdr : list) | null, 7;; tree = node(children : list) | leaf(data : nat) 8;; END; 9 10;;;;;;;;;;; 11;; nat ;; 12;;;;;;;;;;; 13(declare-sort nat 0) 14(declare-fun zero () nat) 15(declare-fun succ (nat) nat) 16 17;;;;;;;;;;;;;;;; 18;; injective 19 20(declare-fun inj1 (nat) nat) 21(assert (forall ((?x1 nat)) 22 (! (= (inj1 (succ ?x1)) ?x1) :pattern ((succ ?x1)) ) )) 23 24 25;;;;;;;;;;;;;;;;;;;; 26;; projection 27 28(declare-fun pred (nat) nat) 29(assert (forall ((?x1 nat)) 30 (! (= (pred (succ ?x1)) ?x1) :pattern ((pred (succ ?x1))) ) )) 31 32(assert (= (pred zero) zero)) 33 34;;;;;;;;;;;;;;;;;;; 35;; test 36(declare-fun is_succ (nat) Bool) 37(assert (= (is_succ zero) false)) 38(assert (forall ((?x1 nat)) 39 (! (= (is_succ (succ ?x1)) true) :pattern ((succ ?x1)) ) )) 40 41(assert (forall ((?x1 nat)) 42 (! (=> (is_succ ?x1) (= ?x1 (succ (pred ?x1)))) :pattern ((is_succ ?x1) (pred ?x1)) ) )) 43 44(declare-fun is_zero (nat) Bool) 45(assert (= (is_zero zero) true)) 46(assert (forall ((?x1 nat)) 47 (! (=> (is_zero ?x1) (= ?x1 zero)) :pattern ((is_zero ?x1)) ) )) 48 49;;; directrr 50(assert (forall ((?x1 nat)) 51 (! (= (is_succ (succ ?x1)) true) :pattern ((is_succ (succ ?x1))) ) )) 52(assert (forall ((?x1 nat)) 53 (! (= (is_zero (succ ?x1)) false) :pattern ((is_zero (succ ?x1))) ))) 54 55 56;;;;;;;;;;;;;;;;;;;; 57;; distinct 58(assert (forall ((?x1 nat)) 59 (! (=> (is_zero ?x1) (not (is_succ ?x1)) ) :pattern ((is_zero ?x1)) ) )) 60(assert (forall ((?x1 nat)) 61 (! (=> (is_succ ?x1) (not (is_zero ?x1)) ) :pattern ((is_succ ?x1)) ) )) 62(assert (forall ((?x1 nat)) 63 (! (=> (not (is_zero ?x1)) (is_succ ?x1) ) :pattern ((is_zero ?x1)) ) )) 64(assert (forall ((?x1 nat)) 65 (! (=> (not (is_succ ?x1)) (is_zero ?x1) ) :pattern ((is_succ ?x1)) ) )) 66 67;;;;;;;;;;;;;;;;;;; 68;; case-split 69(assert (forall ((?x1 nat)) 70 (! (or (is_zero ?x1) (is_succ ?x1)) :pattern ((pred ?x1)) ) )) 71 72;;;;;;;;;;;;;;;;;;; 73;; non-cyclic 74(declare-fun size_nat (nat) Real) 75(assert (forall ((?x1 nat)) 76 (! (> (size_nat (succ ?x1)) (size_nat ?x1)) :pattern ((succ ?x1)) ) )) 77 78 79 80;;;;;;;;;;;;;;;;;;;;; 81;; list and tree 82 83(declare-sort list 0) 84(declare-sort tree 0) 85 86;;;;;;;;;;; 87;; list ;; 88;;;;;;;;;;; 89 90(declare-fun null () list) 91(declare-fun cons (tree list) list) 92 93(declare-fun node (list) tree) 94(declare-fun leaf (nat) tree) 95 96;;;;;;;;;;;;;;;; 97;; injective 98 99(declare-fun inj2 (list) tree) 100(assert (forall ((?x1 tree) (?x2 list)) 101 (! (= (inj2 (cons ?x1 ?x2)) ?x1) :pattern ((cons ?x1 ?x2)) ) )) 102 103(declare-fun inj3 (list) list) 104(assert (forall ((?x1 tree) (?x2 list)) 105 (! (= (inj3 (cons ?x1 ?x2)) ?x2) :pattern ((cons ?x1 ?x2)) ) )) 106 107 108;;;;;;;;;;;;;;;;;;;; 109;; projection 110 111(declare-fun car (list) tree) 112(assert (forall ((?x1 tree) (?x2 list)) 113 (! (= (car (cons ?x1 ?x2)) ?x1) :pattern ((car (cons ?x1 ?x2))) ) )) 114 115(assert (= (car null) (node null))) 116 117(declare-fun cdr (list) list) 118(assert (forall ((?x1 tree) (?x2 list)) 119 (! (= (cdr (cons ?x1 ?x2)) ?x2) :pattern ((cdr (cons ?x1 ?x2))) ) )) 120 121(assert (= (cdr null) null)) 122 123;;;;;;;;;;;;;;;;;;; 124;; test 125(declare-fun is_cons (list) Bool) 126(assert (= (is_cons null) false)) 127(assert (forall ((?x1 tree) (?x2 list)) 128 (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((cons ?x1 ?x2)) ) )) 129 130(assert (forall ((?x1 list)) 131 (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(car ?x1)) ) )) 132(assert (forall ((?x1 list)) 133 (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(cdr ?x1)) ) )) 134 135(declare-fun is_null (list) Bool) 136(assert (= (is_null null) true)) 137 138(assert (forall ((?x1 list)) 139 (! (=> (is_null ?x1) (= (car ?x1) (node null))) :pattern ((is_null ?x1)(car ?x1)) ) )) 140(assert (forall ((?x1 list)) 141 (! (=> (is_null ?x1) (= (cdr ?x1) null)) :pattern ((is_null ?x1)(cdr ?x1)) ) )) 142 143(assert (forall ((?x1 list)) 144 (! (=> (is_null ?x1) (= ?x1 null)) :pattern ((is_null ?x1)) ) )) 145 146;;; directrr 147(assert (forall ((?x1 tree) (?x2 list)) 148 (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((is_cons (cons ?x1 ?x2))) ) )) 149(assert (forall ((?x1 tree) (?x2 list)) 150 (! (= (is_null (cons ?x1 ?x2)) false) :pattern ((is_null (cons ?x1 ?x2))) ) )) 151 152 153 154;;;;;;;;;;;;;;;;;;;; 155;; distinct 156(assert (forall ((?x1 list)) 157 (! (=> (is_null ?x1) (not (is_cons ?x1)) ) :pattern ((is_null ?x1)) ) )) 158(assert (forall ((?x1 list)) 159 (! (=> (is_cons ?x1) (not (is_null ?x1)) ) :pattern ((is_cons ?x1)) ) )) 160(assert (forall ((?x1 list)) 161 (! (=> (not (is_null ?x1)) (is_cons ?x1) ) :pattern ((is_null ?x1)) ) )) 162(assert (forall ((?x1 list)) 163 (! (=> (not (is_cons ?x1)) (is_null ?x1) ) :pattern ((is_cons ?x1)) ) )) 164 165;;;;;;;;;;;;;;;;;;; 166;; case-split 167(assert (forall ((?x1 list)) 168 (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((car ?x1)) ) )) 169(assert (forall ((?x1 list)) 170 (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((cdr ?x1)) ) )) 171 172;;;;;;;;;;;;;;; 173;; tree 174 175;;;;;;;;;;;;;;;; 176;; injective 177 178(declare-fun inj4 (tree) list) 179(assert (forall ((?x1 list)) 180 (! (= (inj4 (node ?x1)) ?x1) :pattern ((node ?x1)) ) )) 181 182(declare-fun inj5 (tree) nat) 183(assert (forall ((?x1 nat)) 184 (! (= (inj5 (leaf ?x1)) ?x1) :pattern ((leaf ?x1)) ) )) 185 186 187;;;;;;;;;;;;;;;;;;;; 188;; projection 189 190(declare-fun children (tree) list) 191(assert (forall ((?x1 list)) 192 (! (= (children (node ?x1)) ?x1) :pattern ((children (node ?x1))) ) )) 193(assert (forall ((?x1 nat)) 194 (! (= (children (leaf ?x1)) null) :pattern ((children (leaf ?x1))) ) )) 195 196 197(declare-fun data (tree) nat) 198(assert (forall ((?x1 nat)) 199 (! (= (data (leaf ?x1)) ?x1) :pattern ((data (leaf ?x1))) ) )) 200(assert (forall ((?x1 list)) 201 (! (= (data (node ?x1)) zero) :pattern ((data (node ?x1))) ) )) 202 203;;;;;;;;;;;;;;;;;;; 204;; test 205(declare-fun is_node (tree) Bool) 206(assert (forall ((?x1 list)) 207 (! (= (is_node (node ?x1)) true) :pattern ((node ?x1)) ) )) 208 209(assert (forall ((?x1 tree)) 210 (! (=> (is_node ?x1) (= ?x1 (node (children ?x1)))) :pattern ((is_node ?x1)(children ?x1)) ) )) 211 212(assert (forall ((?x1 tree)) 213 (! (=> (is_node ?x1) (= (data ?x1) zero)) :pattern ((is_node ?x1)(data ?x1)) ) )) 214 215 216(declare-fun is_leaf (tree) Bool) 217(assert (forall ((?x1 nat)) 218 (! (=> true (= (is_leaf (leaf ?x1)) true)) :pattern ((leaf ?x1)) ) )) 219 220(assert (forall ((?x1 tree)) 221 (! (=> (is_leaf ?x1) (= ?x1 (leaf (data ?x1)))) :pattern ((is_leaf ?x1)(data ?x1)) ) )) 222(assert (forall ((?x1 tree)) 223 (! (=> (is_leaf ?x1) (= (children ?x1) null)) :pattern ((is_leaf ?x1)(children ?x1)) ) )) 224 225;;; directrr 226(assert (forall ((?x1 list)) 227 (! (= (is_node (node ?x1)) true) :pattern ((is_node (node ?x1))) ) )) 228(assert (forall ((?x1 list)) 229 (! (= (is_leaf (node ?x1)) false) :pattern ((is_leaf (node ?x1))) ) )) 230(assert (forall ((?x1 nat)) 231 (! (= (is_leaf (leaf ?x1)) true) :pattern (is_leaf (leaf ?x1)) ) )) 232(assert (forall ((?x1 nat)) 233 (! (= (is_node (leaf ?x1)) false) :pattern ((is_node (leaf ?x1))) ) )) 234 235 236;;;;;;;;;;;;;;;;;;;; 237;; distinct 238(assert (forall ((?x1 tree)) 239 (! (=> (is_node ?x1) (not (is_leaf ?x1)) ) :pattern ((is_node ?x1)) ) )) 240(assert (forall ((?x1 tree)) 241 (! (=> (is_leaf ?x1) (not (is_node ?x1)) ) :pattern ((is_leaf ?x1)) ) )) 242(assert (forall ((?x1 tree)) 243 (! (=> (not (is_node ?x1)) (is_leaf ?x1) ) :pattern ((is_node ?x1)) ) )) 244(assert (forall ((?x1 tree)) 245 (! (=> (not (is_leaf ?x1)) (is_node ?x1) ) :pattern ((is_leaf ?x1)) ) )) 246 247;;;;;;;;;;;;;;;;;;; 248;; case-split 249(assert (forall ((?x1 tree)) 250 (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((children ?x1)) ) )) 251 252(assert (forall ((?x1 tree)) 253 (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((data ?x1)) ) )) 254 255 256;;;;;;;;;;;;;;;;;; 257;; non-cyclic 258(declare-fun size_list (list) Real) 259(declare-fun size_tree (tree) Real) 260(assert (forall ((?x1 tree) (?x2 list)) 261 (! (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) :pattern ((cons ?x1 ?x2)) ) )) 262(assert (forall ((?x1 list)) 263 (! (> (size_tree (node ?x1)) (size_list ?x1)) :pattern ((node ?x1)) ) )) 264(assert (forall ((?x1 nat)) 265 (! (> (size_tree (leaf ?x1)) (size_nat ?x1)) :pattern ((leaf ?x1)) ) )) 266