initialize
call initialize-database 

define sort Bool with constructors
    false :  --> Bool
    true :  --> Bool
    .
declare constructor variables b : Bool.

assume
    { b = false,
      b = true }
    bool-complete
call auto-strategy  bool-complete
call activate-lemma  bool-complete

define sort Nat with constructors
    0 :  --> Nat
    s : Nat --> Nat
    .
declare constructor variables u, v, w, x, y, z : Nat.

declare operators
    leq : Nat Nat --> Bool
    .
assert leq-1 :
    leq(0,y) = true
    .
assert leq-2 :
    leq(s(x),0) = false
    .
assert leq-3 :
    leq(s(x),s(y)) = leq(x,y)
    .

call analyze-operator  leq
call auto-strategy  leq-def-auto
call activate-lemma  leq-def-auto

assume
    { leq(x,y) = true,
      leq(y,x) = true }
    leq-complete
call auto-strategy  leq-complete
call activate-lemma  leq-complete

assume
    { leq(x,x) = true }
    leq-x-x
call auto-strategy  leq-x-x
call activate-lemma  leq-x-x

assume
    { leq(s(x),x) = false }
    leq-sx-x
call auto-strategy  leq-sx-x
call activate-lemma  leq-sx-x

assume
    { leq(x,s(y)) = true,
      leq(x,y) =/= true }
    leq-x-sy
call auto-strategy  leq-x-sy
call activate-lemma  leq-x-sy

assume
    { leq(s(x),y) = false,
      leq(x,y) =/= false }
    leq-sx-y
call auto-strategy  leq-sx-y
call activate-lemma  leq-sx-y

// assume
//     { leq(x,s(x)) = true }
//     leq-x-sx
// call auto-strategy  leq-x-sx
// call activate-lemma  leq-x-sx

assume
    { leq(x,0) =/= true,
      x = 0 }
    leq-x-0
call auto-strategy  leq-x-0
call activate-lemma  leq-x-0

assume
    { leq(x,z) = true,
      leq(x,y) =/= true,
      leq(y,z) =/= true }
    leq-transitive
call auto-strategy  leq-transitive

assume
    { leq(x,y) =/= true,
      leq(y,x) =/= true,
      x = y }
    leq-trichotomy
call auto-strategy  leq-trichotomy

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-0-y
call auto-strategy  plus-0-y
call activate-lemma  plus-0-y

assume
    { plus(s(x),y) = s(plus(x,y)) }
    plus-sx-y
call auto-strategy  plus-sx-y
call activate-lemma  plus-sx-y

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-ass
call auto-strategy  plus-ass
call activate-lemma  plus-ass

assume
    { leq(x,plus(y,z)) = true,
      leq(x,y) =/= true }
    leq-x-plus-mono
call auto-strategy  leq-x-plus-mono
call activate-lemma  leq-x-plus-mono

assume
    { leq(x,plus(x,y)) = true }
    leq-x-plus
call auto-strategy  leq-x-plus
call activate-lemma  leq-x-plus

// assume
//     { leq(s(plus(x,y)),x) = false }
//     leq-s-plus
// call auto-strategy  leq-s-plus
// call activate-lemma  leq-s-plus

assume
    { leq(plus(u,v),plus(x,y)) = true,
      leq(u,x) =/= true,
      leq(v,y) =/= true }
    leq-plus-mono
call auto-strategy  leq-plus-mono
call activate-lemma  leq-plus-mono

assume
    { leq(plus(x,z),plus(y,z)) = leq(x,y) }
    leq-plus-2
call auto-strategy  leq-plus-2
call activate-lemma  leq-plus-2

assume
    { leq(plus(z,x),plus(z,y)) = leq(x,y) }
    leq-plus-1
call simplify  leq-plus-1
call activate-lemma  leq-plus-1

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-0-y
call auto-strategy  times-0-y
call activate-lemma  times-0-y

assume
    { times(s(x),y) = plus(times(x,y),y) }
    times-sx-y
call auto-strategy  times-sx-y
call activate-lemma  times-sx-y

assume
    { times(s(0),x) = x }
    times-s0
call auto-strategy  times-s0
call activate-lemma  times-s0

assume
    { times(x,y) = times(y,x) }
    times-commutative
call auto-strategy  times-commutative
call activate-lemma  times-commutative

assume
    { times(x,plus(y,z)) = plus(times(x,y),times(x,z)) }
    times-plus-distr-1
call auto-strategy  times-plus-distr-1
call activate-lemma  times-plus-distr-1

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-ass
call auto-strategy  times-ass
call activate-lemma  times-ass

assume
    { times(plus(y,z),x) = plus(times(y,x),times(z,x)) }
    times-plus-distr-2
call simplify  times-plus-distr-2

call deactivate-lemmas  { times-plus-distr-1 }

assume
    { leq(times(x,z),times(y,z)) = true,
      leq(x,y) =/= true }
    leq-times-2
call auto-strategy  leq-times-2
call activate-lemma  leq-times-2

assume
    { leq(times(z,x),times(z,y)) = true,
      leq(x,y) =/= true }
    leq-times-1
call simplify  leq-times-1
call activate-lemma  leq-times-1

declare operators
    minus : Nat Nat --> Nat
    .
assert minus-1 :
    minus(x,0) = x
    .
assert minus-2 :
    minus(s(x),s(y)) = minus(x,y)
    .

call analyze-operator  minus
assume
    { def minus(x,y),
      leq(y,x) =/= true }
    def-minus
call auto-strategy  def-minus
call activate-lemma  def-minus

assume
    { minus(x,y) < x,
      y = 0,
      leq(y,x) =/= true }
    minus-ind
call auto-strategy  minus-ind
call activate-lemma  minus-ind

assume
    { minus(x,x) = 0 }
    minus-x-x
call auto-strategy  minus-x-x
call activate-lemma  minus-x-x

assume
    { minus(plus(x,y),y) = x }
    minus-plus-2
call auto-strategy  minus-plus-2
call activate-lemma  minus-plus-2

assume
    { minus(plus(y,x),y) = x }
    minus-plus-1
call simplify  minus-plus-1
call activate-lemma  minus-plus-1

assume
    { minus(plus(x,z),plus(y,z)) = minus(x,y),
      leq(y,x) =/= true }
    minus-plus-3
call auto-strategy  minus-plus-3
call activate-lemma  minus-plus-3

assume
    { minus(plus(z,x),plus(z,y)) = minus(x,y),
      leq(y,x) =/= true }
    minus-plus-4
call simplify  minus-plus-4
call activate-lemma  minus-plus-4

assume
    { plus(y,minus(x,y)) = x,
      leq(y,x) =/= true }
    plus-minus-2
call auto-strategy  plus-minus-2
call activate-lemma  plus-minus-2

assume
    { plus(minus(x,y),y) = x,
      leq(y,x) =/= true }
    plus-minus-1
call auto-strategy  plus-minus-1
call activate-lemma  plus-minus-1

assume
    { times(x,minus(y,z)) = minus(times(x,y),times(x,z)),
      leq(z,y) =/= true }
    times-minus-distr-1
call operators-strategy  { 1 } { [1:2] } times-minus-distr-1

assume
    { leq(minus(x,z),minus(y,z)) = leq(x,y),
      leq(z,x) =/= true,
      leq(z,y) =/= true }
    leq-minus
call auto-strategy  leq-minus
call activate-lemma  leq-minus

declare operators
    div : Nat Nat --> Nat
    .
assert div-1 :
    div(x,y) = 0
    if leq(y,x) =/= true,
       y =/= 0,
       def leq(y,x)
    .
assert div-2 :
    div(x,y) = s(div(minus(x,y),y))
    if
      leq(y,x) = true,
      y =/= 0
    .

call analyze-operator  div
call auto-strategy  div-def-auto
call activate-lemma  div-def-auto

assume
    { div(0,y) = 0,
      y = 0 }
    div-0-y
call operators-strategy  { 1 } { [1] } div-0-y
call activate-lemma  div-0-y

assume
    { div(x,x) = s(0),
      x = 0 }
    div-x-x
call auto-strategy  div-x-x
call activate-lemma  div-x-x

assume
    { div(plus(x,y),x) = s(div(y,x)),
      x = 0 }
    div-plus-1
call operators-strategy  { 1 } { [1] } div-plus-1
call activate-lemma  div-plus-1

assume
    { div(plus(y,x),x) = s(div(y,x)),
      x = 0 }
    div-plus-2
call operators-strategy  { 1 } { [1] } div-plus-2
call activate-lemma  div-plus-2

assume
    { div(times(x,y),x) = y,
      x = 0 }
    div-times-1
call auto-strategy  div-times-1
call activate-lemma  div-times-1

assume
    { div(times(y,x),x) = y,
      x = 0 }
    div-times-2
call simplify  div-times-2
call activate-lemma  div-times-2

assume
    { div(plus(times(x,y),times(x,z)),x) = plus(y,z),
      x = 0 }
    div-plus-times-1
call activate-lemma  times-plus-distr-1 :activate-left-to-right-p FALSE
call simplify  div-plus-times-1
call deactivate-lemmas  { times-plus-distr-1 }
call activate-lemma  div-plus-times-1

assume
    { div(plus(times(y,x),times(z,x)),x) = plus(y,z),
      x = 0 }
    div-plus-times-2
call simplify  div-plus-times-2
call activate-lemma  div-plus-times-2

assume
    { div(minus(times(x,y),times(x,z)),x) = minus(y,z),
      leq(z,y) =/= true,
      x = 0 }
    div-minus-times-1
call activate-lemma  times-minus-distr-1 :activate-left-to-right-p FALSE
call simplify  div-minus-times-1
call deactivate-lemmas  { times-minus-distr-1 }
call activate-lemma  div-minus-times-1

assume
    { leq(div(y,z),div(x,z)) = true,
      leq(y,x) =/= true,
      z = 0 }
    leq-div
call activate-lemma  leq-transitive
call operators-strategy  { 1 1 } { [1:1] [1:2] } leq-div
call deactivate-lemmas  { leq-transitive }
call activate-lemma  leq-div

declare operators
    div-p : Nat Nat --> Bool
    .
assert div-p-1 :
    div-p(x,y) = true
    if x = 0,
       y = 0
    .
assert div-p-2 :
    div-p(x,y) = false
    if x = 0,
       y =/= 0
    .
assert div-p-3 :
    div-p(x,y) = true
    if
      times(x,div(y,x)) = y,
      x =/= 0
    .
assert div-p-4 :
    div-p(x,y) = false
    if
      times(x,div(y,x)) =/= y,
      x =/= 0,
      def times(x,div(y,x))
    .

call analyze-operator  div-p
call operators-strategy  { 1 } { [1] } div-p-def-auto
call activate-lemma  div-p-def-auto

assume
    { div-p(x,0) = true }
    div-p-x-0
call operators-strategy  { 1 } { [1] } div-p-x-0
call activate-lemma  div-p-x-0

assume
    { div-p(x,x) = true }
    div-p-x-x
call operators-strategy  { 1 } { [1] } div-p-x-x
call activate-lemma  div-p-x-x

assume
    { times(y,div(x,y)) = x,
      div-p(y,x) =/= true,
      y = 0 }
    times-div-1
call operators-strategy  { 2 } { [1] } times-div-1
call activate-lemma  times-div-1

assume
    { div(plus(x,y),z) = plus(div(x,z),div(y,z)),
      div-p(z,x) =/= true,
      div-p(z,y) =/= true,
      z = 0 }
    div-plus
apply lemma-rewrite
     1
     [2]
     div-plus-times-1
     1
     [x<-- z, y <-- div(x,z) , z <-- div(y,z)] ..
     div-plus
call cont-proof-attempt :ind-lemmas {}  div-plus
call activate-lemma  div-plus

assume
    { div-p(z,plus(x,y)) = true,
      div-p(z,x) =/= true,
      div-p(z,y) =/= true }
    div-p-plus
call activate-lemmas  { times-plus-distr-1 times-plus-distr-2 }
call operators-strategy  { 1 } { [1] } div-p-plus
call deactivate-lemmas  { times-plus-distr-1 times-plus-distr-2 }
call activate-lemma  div-p-plus

assume
    { div-p(z,times(x,y)) = true,
      div-p(z,x) =/= true }
    div-p-times-1
call auto-strategy  div-p-times-1
call activate-lemma  div-p-times-1

assume
    { div(minus(x,y),z) = minus(div(x,z),div(y,z)),
      div-p(z,x) =/= true,
      div-p(z,y) =/= true,
      leq(y,x) =/= true,
      z = 0 }
    div-minus
apply lemma-rewrite
    1
    [2]
    div-minus-times-1
    1
    [y <-- div(x,z) , z <-- div(y,z), x<--z] ..
    div-minus
call cont-proof-attempt :ind-lemmas {}  div-minus
call activate-lemma  div-minus

assume
    { div-p(z,minus(x,y)) = true,
      div-p(z,x) =/= true,
      div-p(z,y) =/= true,
      leq(x,y) = true }
    div-p-minus
call activate-lemma  times-minus-distr-1
call operators-strategy  { 1 } { [1] } div-p-minus
call deactivate-lemmas  { times-minus-distr-1 }
call activate-lemma  div-p-minus

assume
    { div(times(x,y),z) = times(y,div(x,z)),
      div-p(z,x) =/= true,
      z = 0 }
    div-times-3
call auto-strategy  div-times-3
call activate-lemma  div-times-3

assume
    { div(times(y,x),z) = times(y,div(x,z)),
      div-p(z,x) =/= true,
      z = 0 }
    div-times-4
call simplify  div-times-4
call activate-lemma  div-times-4

assume
    { times(div(x,y),div(y,z)) = div(x,z),
      div-p(y,x) =/= true,
      div-p(z,y) =/= true,
      y = 0,
      z = 0 }
    times-div-2
apply lemma-rewrite
    1
    [1]
    div-times-3
    1
    [y <-- div(x,y) , x <-- y , z <-- z] ..
    times-div-2
call cont-proof-attempt :ind-lemmas {}  times-div-2
call activate-lemma  times-div-2

assume
    { times(div(y,z),div(x,y)) = div(x,z),
       div-p(y,x) =/= true,
       div-p(z,y) =/= true,
       y = 0,
       z = 0 }
    times-div-3
call simplify  times-div-3
call activate-lemma  times-div-3

assume
    { times(x,div(z,x)) = z,
      times(y,div(z,y)) =/= z,
      times(x,div(y,x)) =/= y,
      y = 0,
      x = 0 }
    times-div-trans
apply const-rewrite 1 2 [2] times-div-trans
apply const-rewrite 1 3 [2:1] times-div-trans
call simplify  times-div-trans
call activate-lemma  times-div-trans

assume
    { div-p(x,y) = false,
      leq(x,y) = true,
      y = 0 }
    div-p-leq
call operators-strategy  { 1 } { [1] } div-p-leq

assume
    { div-p(x,y) =/= true,
      div-p(y,x) =/= true,
      x = y }
    div-p-eq
call activate-lemma  leq-trichotomy
call activate-lemma  div-p-leq :obl-litnbs-list {}
call simplify  div-p-eq
call deactivate-lemmas  { leq-trichotomy div-p-leq }

declare operators
    gcd : Nat Nat --> Nat
    .
assert gcd-1 :
    gcd(x,y) = x
    if y = 0,
       x =/= 0
    .
assert gcd-2 :
    gcd(x,y) = y
    if x = 0,
       y =/= 0
    .
assert gcd-3 :
    gcd(x,y) = gcd(x,minus(y,x))
    if
      leq(x,y) = true,
      x =/= 0,
      y =/= 0
    .
assert gcd-4 :
    gcd(x,y) = gcd(minus(x,y),y)
    if
      leq(x,y) =/= true,
      def leq(x,y),
      x =/= 0,
      y =/= 0
    .

call analyze-operator  gcd
assume
    { def gcd(x,y),
      x = 0 }
    def-gcd-1
call operators-strategy  { 1 } { [1] } def-gcd-1
call activate-lemma  def-gcd-1
assume
    { def gcd(x,y),
      y = 0 }
    def-gcd-2
call operators-strategy  { 1 } { [1] } def-gcd-2
call activate-lemma  def-gcd-2

assume
    { gcd(x,y) =/= 0,
      x = 0 }
    gcd-x-0
call auto-strategy  gcd-x-0
call activate-lemma  gcd-x-0

assume
    { gcd(x,y) =/= 0,
      y = 0 }
    gcd-y-0
call auto-strategy  gcd-y-0
call activate-lemma  gcd-y-0

assume
    { gcd(x,x) = x,
      x = 0 }
    gcd-idempotent
call operators-strategy  { 1 } { [1] } gcd-idempotent
call activate-lemma  gcd-idempotent

assume
    { gcd(x,y) = gcd(y,x),
      x = 0 }
    gcd-commutative
call activate-lemma  leq-trichotomy
call auto-strategy  gcd-commutative
call deactivate-lemmas  { leq-trichotomy }

assume
    { div-p(gcd(x,y),x) = true,
      y = 0 }
    div-p-gcd-1
assume
    { div-p(gcd(x,y),y) = true,
      x = 0 }
    div-p-gcd-2

set weight (x,y) div-p-gcd-1
set weight (x,y) div-p-gcd-2
call operators-strategy  { 1 } { [1:1] } div-p-gcd-1
apply lemma-subs
    div-p-plus
    [z <-- gcd(minus(x,y),y) , x <-- minus(x,y)] ..
    div-p-gcd-1
call cont-proof-attempt :ind-lemmas { div-p-gcd-1 div-p-gcd-2 } div-p-gcd-1
call operators-strategy  { 1 } { [1:1] } div-p-gcd-2
apply lemma-subs
    div-p-plus
    [z <-- gcd(x,minus(y,x)) , y <-- minus(y,x)] ..
    div-p-gcd-2
call cont-proof-attempt :ind-lemmas { div-p-gcd-1 div-p-gcd-2 } div-p-gcd-2

call activate-lemma  div-p-gcd-1
call activate-lemma  div-p-gcd-2

assume
    { div-p(z,gcd(x,y)) = true,
      div-p(z,x) =/= true,
      div-p(z,y) =/= true,
      x = 0 }
    div-p-gcd-3
call activate-lemma  leq-trichotomy
call auto-strategy  div-p-gcd-3
call deactivate-lemmas  { leq-trichotomy }
call activate-lemma  div-p-gcd-3

assume
    { div-p(x,z) = true,
      div-p(x,y) =/= true,
      div-p(y,z) =/= true }
    div-p-trans
call operators-strategy  { 1 2 3 } { [1] [1] [1] } div-p-trans
call activate-lemma  div-p-trans

assume
    { div-p(gcd(x,y),z) = true,
      div-p(x,z) =/= true,
      x = 0 }
    div-p-gcd-trans-1
call simplify  div-p-gcd-trans-1
call activate-lemma  div-p-gcd-trans-1

assume
    { div-p(gcd(x,y),z) = true,
      div-p(y,z) =/= true,
      y = 0 }
    div-p-gcd-trans-2
call simplify  div-p-gcd-trans-2
call activate-lemma  div-p-gcd-trans-2

call change-lemmas-order  { bool-complete leq-def-auto leq-complete leq-x-x leq-sx-x leq-x-sy leq-sx-y leq-x-0 plus-def-auto plus-0-y plus-sx-y plus-commutative plus-comm-ext plus-ass leq-x-plus-mono leq-x-plus leq-plus-mono leq-plus-2 leq-plus-1 times-def-auto times-0-y times-sx-y times-s0 times-commutative times-comm-ext times-ass leq-times-2 leq-times-1 def-minus minus-ind minus-x-x minus-plus-2 minus-plus-1 minus-plus-3 minus-plus-4 plus-minus-2 plus-minus-1 leq-minus div-def-auto div-0-y div-x-x div-plus-1 div-plus-2 div-times-1 div-times-2 div-plus-times-1 div-plus-times-2 div-minus-times-1 leq-div div-p-def-auto div-p-x-0 div-p-x-x times-div-1 div-plus div-p-plus div-p-times-1 div-minus div-p-minus div-times-3 div-times-4 times-div-2 times-div-3 times-div-trans def-gcd-1 def-gcd-2 gcd-x-0 gcd-y-0 gcd-idempotent div-p-gcd-trans-1 div-p-gcd-trans-2 div-p-gcd-1 div-p-gcd-2 div-p-gcd-3 }

assume
    { div-p(gcd(gcd(x,y),z),gcd(x,gcd(y,z))) = true,
      x = 0,
      y = 0,
      z = 0 }
    div-p-gcd-4
call simplify  div-p-gcd-4
call activate-lemma  div-p-gcd-4

assume
    { div-p(gcd(x,gcd(y,z)),gcd(gcd(x,y),z)) = true,
      x = 0,
      y = 0,
      z = 0 }
    div-p-gcd-5
call simplify  div-p-gcd-5
call activate-lemma  div-p-gcd-5

assume
    { gcd(gcd(x,y),z) = gcd(x,gcd(y,z)),
      x = 0,
      y = 0,
      z = 0 }
    gcd-ass
apply lemma-subs
    div-p-eq
    [x <-- gcd(gcd(x,y),z) , y <-- gcd(x,gcd(y,z))] ..
    gcd-ass
call cont-proof-attempt :ind-lemmas {}  gcd-ass
call activate-lemma  gcd-ass