Invalid Verification Condition in Relational Logic

bindings
  (v_15 :  'a tree,
	 x_0 :  'a tree,
	 t :  'a tree,
	 anc_1047 :  'a tree,
	 z : 'a,
	 d :  'a tree,
	 a :  'a tree,
	 x : 'a,
	 anc_1045 :  'a tree,
	 b :  'a tree,
	 y : 'a,
	 c :  'a tree,
	 anc_1056 :  'a tree,
	 anc_1063 :  'a tree,
	 Rmem1 : ({(1 :  'a tree, 2 : 'a)}) -> ( bool),
	 Rtos0 : ({(1 :  'a tree, 2 : 'a, 3 : 'a)}) -> ( bool))
in
      t = x_0
      Rtos0(t) = (((Rmem1(anc_1047) X {(z)})
               U (({(z)} X Rmem1(d))
               U (Rmem1(anc_1047) X Rmem1(d))))
               U (Rtos0(d)
               U (Rtos0(anc_1047)
               U {()})))
      Rmem1(t) = ({(z)}
               U (Rmem1(d)
               U (Rmem1(anc_1047)
               U {()})))
      Rtos0(anc_1063) = (((Rmem1(b) X {(z)})
                      U (({(z)} X Rmem1(d))
                      U (Rmem1(b) X Rmem1(d))))
                      U (Rtos0(d)
                      U (Rtos0(b)
                      U {()})))
      Rmem1(anc_1063) = ({(z)}
                      U (Rmem1(d)
                      U (Rmem1(b)
                      U {()})))
      Rtos0(anc_1056) = (((Rmem1(a) X {(x)})
                      U (({(x)} X Rmem1(c))
                      U (Rmem1(a) X Rmem1(c))))
                      U (Rtos0(c)
                      U (Rtos0(a)
                      U {()})))
      Rmem1(anc_1056) = ({(x)}
                      U (Rmem1(c)
                      U (Rmem1(a)
                      U {()})))
      Rtos0(anc_1045) = (((Rmem1(b) X {(y)})
                      U (({(y)} X Rmem1(c))
                      U (Rmem1(b) X Rmem1(c))))
                      U (Rtos0(c)
                      U (Rtos0(b)
                      U {()})))
      Rmem1(anc_1045) = ({(y)}
                      U (Rmem1(c)
                      U (Rmem1(b)
                      U {()})))
      Rtos0(anc_1047) = (((Rmem1(a) X {(x)})
                      U (({(x)} X Rmem1(anc_1045))
                      U (Rmem1(a) X Rmem1(anc_1045))))
                      U (Rtos0(anc_1045)
                      U (Rtos0(a) U {()})))
      Rmem1(anc_1047) = ({(x)}
                      U (Rmem1(anc_1045)
                      U (Rmem1(a)
                      U {()})))
      Rtos0(v_15) = (((Rmem1(anc_1056) X {(y)})
                  U (({(y)} X Rmem1(anc_1063))
                  U (Rmem1(anc_1056) X Rmem1(anc_1063))))
                  U (Rtos0(anc_1063)
                  U (Rtos0(anc_1056)
                  U {()})))
      Rmem1(v_15) = ({(y)}
                  U (Rmem1(anc_1063)
                  U (Rmem1(anc_1056)
                  U {()})))
   =>
      Rtos0(v_15) = Rtos0(x_0)
end