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 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,x) = true } leq-x-x call auto-strategy leq-x-x call activate-lemma leq-x-x assume { leq(x,s(y)) = true, leq(x,y) =/= true } leq-s call auto-strategy leq-s call activate-lemma leq-s assume { x < y, leq(x,y) =/= true, x = y } leq-ind call variables-strategy { x y } leq-ind call activate-lemma leq-ind assume { x < y, leq(s(x),y) =/= true } leq-s-ind call auto-strategy leq-s-ind call activate-lemma leq-s-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-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(plus(x,z),plus(y,z)) = leq(x,y) } leq-plus-mon-2 call auto-strategy leq-plus-mon-2 call activate-lemma leq-plus-mon-2 assume { leq(plus(z,x),plus(z,y)) = leq(x,y) } leq-plus-mon-1 call simplify leq-plus-mon-1 call activate-lemma leq-plus-mon-1 assume { leq(x,plus(y,z)) = true, leq(x,y) =/= true } leq-plus-trans-2 call auto-strategy leq-plus-trans-2 call activate-lemma leq-plus-trans-2 assume { leq(x,plus(z,y)) = true, leq(x,y) =/= true } leq-plus-trans-1 call simplify leq-plus-trans-1 call activate-lemma leq-plus-trans-1 assume { leq(x,plus(x,y)) = true } leq-plus-2 call simplify leq-plus-2 call activate-lemma leq-plus-2 assume { leq(x,plus(y,x)) = true } leq-plus-1 call simplify leq-plus-1 call activate-lemma leq-plus-1 define sort State with constructors start : --> State update : Nat Nat State --> State . declare constructor variables S : State. declare operators lookup : Nat State --> Nat . assert lookup-1 : lookup(x,start) = 0 . assert lookup-2 : lookup(x,update(y,z,S)) = z if x = y . assert lookup-3 : lookup(x,update(y,z,S)) = lookup(x,S) if x =/= y . call analyze-operator lookup call auto-strategy lookup-def-auto call activate-lemma lookup-def-auto define sort Expr with constructors nat : Nat --> Expr id : Nat --> Expr add : Expr Expr --> Expr appl : Expr Nat Expr --> Expr . declare constructor variables e, e1, e2, e3 : Expr. declare operators nb-appl : Expr --> Nat . assert nb-appl-1 : nb-appl(nat(x)) = 0 . assert nb-appl-2 : nb-appl(id(x)) = 0 . assert nb-appl-3 : nb-appl(add(e1,e2)) = plus(nb-appl(e1),nb-appl(e2)) . assert nb-appl-4 : nb-appl(appl(e1,x,e2)) = s(plus(nb-appl(e1),nb-appl(e2))) . call analyze-operator nb-appl call auto-strategy nb-appl-def-auto call activate-lemma nb-appl-def-auto declare operators exp : Expr Nat Expr --> Expr exhelp : Expr --> Expr . assert exp-1 : exp(nat(x),y,e) = nat(x) . assert exp-2 : exp(id(x),y,e) = id(x) if x =/= y . assert exp-3 : exp(id(x),y,e) = exhelp(e) if x = y . assert exp-4 : exp(add(e1,e2),y,e) = add(exp(e1,y,e),exp(e2,y,e)) . assert exp-5 : exp(appl(e1,x,e2),y,e) = exp(exp(e1,x,e2),y,e) . assert exhelp-1 : exhelp(nat(x)) = nat(x) . assert exhelp-2 : exhelp(id(x)) = id(x) . assert exhelp-3 : exhelp(add(e1,e2)) = add(exhelp(e1),exhelp(e2)) . assert exhelp-4 : exhelp(appl(e1,x,e2)) = exp(e1,x,e2) . call analyze-operator exp assume { def exp(e1,x,e2) } def-exp call analyze-operator exhelp assume { nb-appl(exp(e1,x,e2)) = 0 } nb-appl-exp assume { nb-appl(exhelp(e)) = 0 } nb-appl-exhelp set weight (nb-appl(appl(e1,x,e2)),appl(e1,x,e2)) def-exp set weight (nb-appl(e1),e1,0) exhelp-def-auto set weight (nb-appl(appl(e1,x,e2)),appl(e1,x,e2)) nb-appl-exp set weight (nb-appl(e),e,0) nb-appl-exhelp call operators-strategy { 1 } { [1] } :ind-lemmas { def-exp exhelp-def-auto nb-appl-exp nb-appl-exhelp } def-exp call auto-strategy :ind-lemmas { def-exp exhelp-def-auto nb-appl-exp nb-appl-exhelp } exhelp-def-auto call operators-strategy { 1 } { [1:1] } :ind-lemmas { def-exp exhelp-def-auto nb-appl-exp nb-appl-exhelp } nb-appl-exp call auto-strategy :ind-lemmas { def-exp exhelp-def-auto nb-appl-exp nb-appl-exhelp } nb-appl-exhelp call activate-lemmas { def-exp exhelp-def-auto nb-appl-exp nb-appl-exhelp } declare operators eval : Expr State --> Nat . assert eval-1 : eval(nat(x),S) = x . assert eval-2 : eval(id(x),S) = lookup(x,S) . assert eval-3 : eval(add(e1,e2),S) = plus(eval(e1,S),eval(e2,S)) . assert eval-4 : eval(appl(e1,x,e2),S) = eval(e1,update(x,eval(e2,S),S)) . call analyze-operator eval call auto-strategy eval-def-auto call activate-lemma eval-def-auto assume { eval(exp(e1,x,e2),S) = eval(e1,update(x,eval(e2,S),S)) } eval-exp assume { eval(exhelp(e),S) = eval(e,S) } eval-exhelp set weight (nb-appl(appl(e1,x,e2)),appl(e1,x,e2)) eval-exp set weight (nb-appl(e),e,0) eval-exhelp call operators-strategy { 1 } { [1:1] } :ind-lemmas { eval-exp eval-exhelp } eval-exp call auto-strategy :ind-lemmas { eval-exp eval-exhelp } eval-exhelp call activate-lemmas { eval-exp eval-exhelp }