;;Proof Obligations of Module in Harvey/SMT Language
(benchmark switch1Operation2

	   :logic UNKNOWN

 	   ;; todos os nomes globais a maquina devem ser declarados como extrafuns ou extrapreds
	   ;; junto com o tipo deles.
	   ;; devem ser declarados como extrapreds todos os nomes cujo tipo é conjunto
	   :extrafuns ((normal Int)
		       (reverse Int)
		       (void Int)
		       (actual_pos Int))
	   :extrapreds ((POSITION Int))
	   ;; colocar aqui as extramacros definindo as operações sobre conjuntos

	   ;;OPERATIONS
	   :formula
	   (not
	    (implies
	     (and 
	      (in normal POSITION)
	      (in void POSITION)
	      (in reverse POSITION)
	      (distinct normal void reverse))
	     (forall (m1 Int) (m2 Int) (m3 Int) 
		     (implies 
		      (and 
		       (in actual_pos POSITION) 
		       (and (in m1 POSITION) (in m2 POSITION) (in m3 POSITION))) 
		      (flet ((set0 (union (singleton m1) (union (singleton m2) (singleton m3)))))
			(and 
			 (implies (and (in normal set0)
				       (not (in reverse set0)))
			   (in normal POSITION)) 
			 (implies (and (in reverse set0) 
				       (not (in normal set0)))
			   (in reverse POSITION)) 
			 (implies (not (or (and (in normal set0) 
						(not (in reverse set0)))
					   (and (in reverse set0) 
						(not (in normal set0)))))
			   (in void POSITION)))))
		     )))
)