initialize call initialize-database define sort bool with constructors true : --> bool false : --> bool . declare constructor variables b : bool. assume { b = true, b = false } bool-complete call auto-strategy bool-complete call activate-lemma bool-complete declare operators not : bool --> bool . assert not-1 : not(true) = false . assert not-2 : not(false) = true . call analyze-operator not call auto-strategy not-def-auto call activate-lemma not-def-auto assume { not(b) = true, b = true } not-b-true call auto-strategy not-b-true call activate-lemma not-b-true assume { not(b) = false, b = false } not-b-false call auto-strategy not-b-false call activate-lemma not-b-false assume { not(not(b)) = b } not-not-b call auto-strategy not-not-b call activate-lemma not-not-b define sort nat with constructors 0 : --> nat s : nat --> nat . declare constructor variables w,x,y,z : nat. declare operators even : nat --> bool . assert even-1 : even(0) = true . assert even-2 : even(s(x)) = not(even(x)) . call analyze-operator even call auto-strategy even-def-auto call activate-lemma even-def-auto declare operators half : nat --> nat . assert half-1 : half(0) = 0 . assert half-2 : half(s(s(x))) = s(half(x)) . call analyze-operator half :speculate-domain-lemma-p FALSE assume { def half(x), even(x) =/= true } def-half call auto-strategy def-half call activate-lemma def-half assume { half(x) =/= 0, even(x) =/= true, x = 0 } half-0 call auto-strategy half-0 call activate-lemma half-0 assume { half(x) < x, even(x) =/= true, x = 0 } half-ind call auto-strategy half-ind call activate-lemma half-ind declare operators plus : nat nat --> nat . assert plus-1 : plus(x,0)=x . assert plus-2 : plus(x,s(y))=s(plus(x,y)) . call analyze-operator plus call auto-strategy plus-def-auto call activate-lemma plus-def-auto assume { plus(0,y)=y } plus-3 call auto-strategy plus-3 call activate-lemma plus-3 assume { plus(s(x),y)=s(plus(x,y)) } plus-4 call auto-strategy plus-4 call activate-lemma plus-4 assume { plus(x,y)=plus(y,x) } plus-commutative call auto-strategy plus-commutative call activate-lemma plus-commutative assume { plus(x,plus(y,z))=plus(y,plus(x,z)) } plus-comm-ext call auto-strategy plus-comm-ext call activate-lemma plus-comm-ext assume { plus(plus(x,y),z)=plus(x,plus(y,z)) } plus-associative call auto-strategy plus-associative call activate-lemma plus-associative assume { even(plus(x,y)) = even(y), even(x) =/= true } even-plus-1 call auto-strategy even-plus-1 call activate-lemma even-plus-1 assume { even(plus(x,y)) = not(even(y)), even(x) = true } even-plus-2 call auto-strategy even-plus-2 call activate-lemma even-plus-2 assume { even(x) = true, x =/= plus(y,y) } even-x-2-y call simplify even-x-2-y call activate-lemma even-x-2-y :head-litnbs { 2 } assume { plus(half(x),half(y)) = half(plus(x,y)), even(x) =/= true, even(y) =/= true } plus-half-x-y call auto-strategy plus-half-x-y call activate-lemma plus-half-x-y assume { half(plus(x,x)) = x } half-plus-x-x call auto-strategy half-plus-x-x call activate-lemma half-plus-x-x declare operators times : nat nat --> nat . assert times-1 : times(x,0)=0 . assert times-2 : times(x,s(y))=plus(times(x,y),x) . call analyze-operator times call auto-strategy times-def-auto call activate-lemma times-def-auto assume { times(0,y)=0 } times-3 call auto-strategy times-3 call activate-lemma times-3 assume { times(s(x),y)=plus(times(x,y),y) } times-4 call auto-strategy times-4 call activate-lemma times-4 assume { times(plus(x,y),z)=plus(times(x,z),times(y,z)) } times-plus-distributive-1 call auto-strategy times-plus-distributive-1 call activate-lemma times-plus-distributive-1 assume { times(x,plus(y,z))=plus(times(x,y),times(x,z)) } times-plus-distributive-2 call auto-strategy times-plus-distributive-2 call activate-lemma times-plus-distributive-2 assume { times(x,y)=times(y,x) } times-commutative call auto-strategy times-commutative call activate-lemma times-commutative assume { times(x,times(y,z))=times(y,times(x,z)) } times-comm-ext call auto-strategy times-comm-ext call activate-lemma times-comm-ext assume { times(times(x,y),z)=times(x, times(y,z)) } times-associative call auto-strategy times-associative call activate-lemma times-associative assume { even(times(x,y)) = true, even(x) =/= true } even-times-1 call auto-strategy even-times-1 call activate-lemma even-times-1 assume { even(times(y,x)) = true, even(x) =/= true } even-times-2 call auto-strategy even-times-2 call activate-lemma even-times-2 assume { even(times(x,x)) = even(x) } even-x2 call auto-strategy even-x2 call activate-lemma even-x2 assume { even(x) = true, times(x,x) =/= plus(y,y) } even-x-x2-2y call simplify even-x-x2-2y call activate-lemma even-x-x2-2y assume { times(half(x),y) = half(times(x,y)), even(x) =/= true } times-half-1 call auto-strategy times-half-1 call activate-lemma times-half-1 :activate-left-to-right-p FALSE assume { times(y,half(x)) = half(times(y,x)), even(x) =/= true } times-half-2 call auto-strategy times-half-2 assume { even(half(times(x,x))) = true, even(x) =/= true } even-half-x2 call simplify even-half-x2 call activate-lemmas { times-half-1 times-half-2 even-half-x2 } assume { plus(times(half(x),half(x)),plus(times(half(x),half(x)),plus(times(half(x),half(x)),times(half(x),half(x))))) = times(x,x), even(x) =/= true } 4-half-x2 call simplify 4-half-x2 call activate-lemma 4-half-x2 assume { plus(times(half(x),half(x)),times(half(x),half(x))) = times(y,y), times(x,x) =/= plus(times(y,y),times(y,y)) } 2-halfx2 apply lit-add even(x) =/= true half(plus(times(half(x),half(x)),plus(times(half(x),half(x)),plus(times(half(x),half(x)),times(half(x),half(x)))))) = half(plus(times(y,y),times(y,y))) . .. 2-halfx2 call simplify 2-halfx2 call simplify 2-halfx2 apply const-rewrite 1 4 [2:1] 2-halfx2 call simplify 2-halfx2 call activate-lemma 2-halfx2 assume { times(x,x) =/= plus(times(y,y),times(y,y)), y = 0 } irrat-2 call auto-strategy irrat-2