blob: fb6998d71d839f2e21640c487ab317684a8d0817 (
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
74
75
76
77
78
79
|
; COMMAND-LINE: -q
; EXPECT: sat
(set-logic QF_ALL)
(set-info :status sat)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Datatype declarations
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-datatypes ((ColorType 0))
(((ColorType_Red) (ColorType_Black))
))
(declare-datatypes ((RBTree 0) (RBTree_Node_recd 0))
(((RBTree_Leaf) (RBTree_Node (destRBTree_Node RBTree_Node_recd)))
((RBTree_Node_recd (RBTree_Node_recd_color ColorType)
(RBTree_Node_recd_left RBTree) (RBTree_Node_recd_elem Int)
(RBTree_Node_recd_right RBTree)))
))
(declare-datatypes ((BoolColor 0))
(((BoolColor (BoolColor_res Bool) (BoolColor_color ColorType)))
))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Uninterpreted symbols
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-fun v0 () Int)
(declare-fun t () RBTree)
;; (declare-fun NoTwoRedsFn (RBTree) BoolColor)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Defined symbols
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-fun assembleFn ((ll RBTree) (le Int) (lr RBTree) (e Int) (rl RBTree) (re Int) (rr RBTree)) RBTree
(RBTree_Node (RBTree_Node_recd ColorType_Red (RBTree_Node (RBTree_Node_recd ColorType_Black ll le lr)) e (RBTree_Node (RBTree_Node_recd ColorType_Black rl re rr)))))
(define-fun balanceFn ((c ColorType) (left RBTree) (elem Int) (right RBTree)) RBTree
(ite (= c ColorType_Black) (ite (not (ite ((_ is RBTree_Leaf) left) false (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) true false)) true))) (ite ((_ is RBTree_Leaf) right) (ite ((_ is RBTree_Leaf) left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node right))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node right))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node right))) (ite ((_ is RBTree_Leaf) left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) ColorType_Red)) (assembleFn left elem (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node right)) (RBTree_Node_recd_right (destRBTree_Node right))) (ite ((_ is RBTree_Leaf) left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node right)))) ColorType_Red)) (assembleFn left elem (RBTree_Node_recd_left (destRBTree_Node right)) (RBTree_Node_recd_elem (destRBTree_Node right)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node right)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node right))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node right))) (ite ((_ is RBTree_Leaf) left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) ColorType_Red)) (assembleFn left elem (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node right)) (RBTree_Node_recd_right (destRBTree_Node right))) (ite ((_ is RBTree_Leaf) left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node right))) (ite ((_ is RBTree_Leaf) left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node right)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) ColorType_Red)) (assembleFn left elem (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node right)))) (RBTree_Node_recd_elem (destRBTree_Node right)) (RBTree_Node_recd_right (destRBTree_Node right))) (ite ((_ is RBTree_Leaf) left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))))))) (ite ((_ is RBTree_Leaf) left) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (not (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) false (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) true false))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_right (destRBTree_Node left))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node left)) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_right (destRBTree_Node left)))) elem right) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)))))) (ite ((_ is RBTree_Leaf) (RBTree_Node_recd_left (destRBTree_Node left))) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right)) (ite (and (= (RBTree_Node_recd_color (destRBTree_Node left)) ColorType_Red) (= (RBTree_Node_recd_color (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) ColorType_Red)) (assembleFn (RBTree_Node_recd_left (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_right (destRBTree_Node (RBTree_Node_recd_left (destRBTree_Node left)))) (RBTree_Node_recd_elem (destRBTree_Node left)) (RBTree_Node_recd_right (destRBTree_Node left)) elem right) (RBTree_Node (RBTree_Node_recd ColorType_Black left elem right))))))) (RBTree_Node (RBTree_Node_recd c left elem right))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Catamorphisms
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
( declare-fun memberFn ( Int RBTree ) Bool )
( declare-fun EqualBlackPathsFn ( RBTree ) Int )
( declare-fun insFn ( Int RBTree ) RBTree )
( declare-fun insertFn ( Int RBTree ) RBTree )
( declare-fun NoTwoRedsFn ( RBTree ) BoolColor )
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Goals
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;(push)
(assert (and ((_ is RBTree_Leaf) t)
(and (not ((_ is RBTree_Leaf) (insertFn v0 t)))
(not (BoolColor_res (NoTwoRedsFn (RBTree_Node_recd_left (destRBTree_Node (insertFn v0 t)))))))))
;;(pop)
( assert ( = ( insertFn v0 t ) ( ite ( (_ is RBTree_Leaf) ( insFn v0 t ) ) ( insFn v0 t ) ( RBTree_Node ( RBTree_Node_recd ColorType_Black ( RBTree_Node_recd_left ( destRBTree_Node ( insFn v0 t ) ) ) ( RBTree_Node_recd_elem ( destRBTree_Node ( insFn v0 t ) ) ) ( RBTree_Node_recd_right ( destRBTree_Node ( insFn v0 t ) ) ) ) ) ) ) )
( assert ( = ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ( ite ( (_ is RBTree_Leaf) ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ) )
( assert ( = ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ( ite ( (_ is RBTree_Leaf) ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 t ) ) ) ) ) ) ) ) )
( assert ( = ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ( ite ( (_ is RBTree_Leaf) ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) )
( assert ( = ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ( ite ( (_ is RBTree_Leaf) ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) )
( assert ( = ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ( ite ( (_ is RBTree_Leaf) ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ( RBTree_Node ( RBTree_Node_recd ColorType_Black ( RBTree_Node_recd_left ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ( RBTree_Node_recd_elem ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ( RBTree_Node_recd_right ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ) ) )
( assert ( = ( NoTwoRedsFn ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ( ite ( (_ is RBTree_Leaf) ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_right ( destRBTree_Node t ) ) ) ) ) ) ) ) )
( assert ( = ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ( ite ( (_ is RBTree_Leaf) ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ( RBTree_Node ( RBTree_Node_recd ColorType_Black ( RBTree_Node_recd_left ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ( RBTree_Node_recd_elem ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ( RBTree_Node_recd_right ( destRBTree_Node ( insFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ) ) )
( assert ( = ( NoTwoRedsFn ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ( ite ( (_ is RBTree_Leaf) ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ( BoolColor true ColorType_Black ) ( BoolColor ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ( and ( BoolColor_res ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ( or ( not ( = ( RBTree_Node_recd_color ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ColorType_Red ) ) ( and ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_left ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ColorType_Red ) ) ( not ( = ( BoolColor_color ( NoTwoRedsFn ( RBTree_Node_recd_right ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ColorType_Red ) ) ) ) ) ) ( RBTree_Node_recd_color ( destRBTree_Node ( insertFn v0 ( RBTree_Node_recd_left ( destRBTree_Node t ) ) ) ) ) ) ) ) )
( check-sat )
|
