initialize
call initialize-database
call set-default-settings :allow-alternative-free-var-bindings-p FALSE
declare sorts Bool.
define sort Bool with constructors
    true :  --> Bool
    false :  --> Bool
    .
declare constructor variables 
    b, b1, b2, b3, b4 : Bool.

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

declare operators
    and : Bool Bool --> Bool
    .
assert and-1 :
    and(true,b2) = b2
    .
assert and-2 :
    and(false,b2) = false
    .

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

assume
    { and(b1,b2) = and(b2,b1) }
    and-commutative
call auto-strategy :recursive-strategy-p TRUE  and-commutative
call activate-lemma  and-commutative

assume
    { and(b1,and(b2,b3)) = and(b2,and(b1,b3)) }
    and-extended-commutativity
call auto-strategy  and-extended-commutativity
call activate-lemma  and-extended-commutativity

assume
    { and(and(b1,b2),b3) = and(b1,and(b2,b3)) }
    and-associative
call auto-strategy  and-associative
call activate-lemma  and-associative

assume
    { and(b1,b2) = false,
      b1 = true }
    and-true
call auto-strategy  and-true
call activate-lemma  and-true

declare operators
    or : Bool Bool --> Bool
    .
assert or-1 :
    or(true,b2) = true
    .
assert or-2 :
    or(false,b2) = b2
    .

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

assume
    { or(b1,b2) = or(b2,b1) }
    or-commutative
call auto-strategy :recursive-strategy-p TRUE  or-commutative
call activate-lemma  or-commutative

assume
    { or(b1,or(b2,b3)) = or(b2,or(b1,b3)) }
    or-extended-commutativity
call auto-strategy  or-extended-commutativity
call activate-lemma  or-extended-commutativity

assume
    { or(or(b1,b2),b3) = or(b1,or(b2,b3)) }
    or-associative
call auto-strategy  or-associative
call activate-lemma  or-associative

assume
    { or(b1,b2) = b2,
      b1 = true }
    or-false
call auto-strategy  or-false
call activate-lemmas  { or-false }

declare sorts Nat.
define sort Nat with constructors
    0 :  --> Nat
    S : Nat --> Nat
    .
declare operators
    gt-nat : Nat Nat --> Bool
    .
declare constructor variables 
    n, m, n1, n2, n3, n4, m1, m2, m3, m4 : Nat
    .
//assume
//    { S(n) =/= S(m), n = m }
//    S-lemma
//call auto-strategy  S-lemma
//call activate-lemma  S-lemma
assert
 gt-nat-1 :
    gt-nat(S(n),0) = true
 gt-nat-2 :
    gt-nat(S(n),S(m)) = gt-nat(n,m)
 gt-nat-3 :
    gt-nat(0,n) = false
    .
call analyze-operator  gt-nat
call auto-strategy  gt-nat-def-auto
call activate-lemma  gt-nat-def-auto
assume
    { gt-nat(n,m) = true,
      gt-nat(n,n1) =/= true,
      gt-nat(n1,m) =/= true }
    gt-nat-trans
call auto-strategy  gt-nat-trans
call activate-lemma  gt-nat-trans
assume
    { gt-nat(n,n) = false }
    gt-nat-irrefl
call auto-strategy  gt-nat-irrefl
call activate-lemma  gt-nat-irrefl
declare sorts FID.
define sort FID with constructors
    Fid : Nat Nat --> FID
    .
declare constructor variables 
    f, g, h, f1, f2, f3, f4 : FID
    .
declare operators
    arity : FID --> Nat
    prec : FID FID --> Bool
    .
assert
  prec-1:
    prec(Fid(n,m),Fid(n1,m1)) = gt-nat(n,n1)
    .
call analyze-operator  prec
call auto-strategy  prec-def-auto
call activate-lemma  prec-def-auto
assume
    { prec(f,g) = true,
      prec(f,h) =/= true,
      prec(h,g) =/= true }
    prec-trans
call auto-strategy  prec-trans
call activate-lemma  prec-trans
assume
    { prec(f,f) = false }
    prec-irrefl
call auto-strategy  prec-irrefl
call activate-lemma  prec-irrefl
assert
 arity-1 :
    arity(Fid(n,m)) = m
    .
call analyze-operator  arity
call auto-strategy  arity-def-auto
call activate-lemma  arity-def-auto
declare sorts VID.
define sort VID with constructors
    Vid : Nat --> VID
    .
declare constructor variables 
    x, y, z, x1, x2, x3, x4 : VID
    .
declare sorts Term.
declare sorts Termlist.
define sort Term with constructors
    V : VID --> Term
    F : FID Termlist --> Term
    .
define sort Termlist with constructors
    nil :  --> Termlist
    cons : Term Termlist --> Termlist
    .
declare constructor variables
    ss, ts, us, vs, ts1, ts2, ts3, ts4, ss1 : Termlist.
declare constructor variables
    s, t, u, v, t1, t2, t3, t4 : Term.
declare operators
    length : Termlist --> Nat
    .
assert
 length-1 :
    length(nil) = 0
 length-2 :
    length(cons(t,ts)) = S(length(ts))
    .
call analyze-operator  length
call auto-strategy  length-def-auto
call activate-lemma  length-def-auto
//assume
//    { arity(g) =/= length(ss),
//      arity(g) =/= length(ts),
//      length(ss) = length(ts) }
//    length-arity
//call simplify  length-arity
//call activate-lemma  length-arity
declare operators
    Fun : Term --> Bool
    Var : Term --> Bool
    .
assert
 Fun-1 :
    Fun(F(f,ss)) = true
 Fun-2 :
    Fun(V(x)) = false
 Var-1 :
    Var(V(x)) = true
 Var-2 :
    Var(F(f,ss)) = false
    .
call analyze-operator Fun
call analyze-operator Var
call auto-strategy Fun-def-auto
call auto-strategy Var-def-auto
call activate-lemmas { Fun-def-auto Var-def-auto }
declare operators
    Well : Term --> Bool
    Well_tl : Termlist --> Bool
    .
assert
 Well-1 :
    Well(V(x)) = true
 Well-2 :
    Well(F(f,ss)) = Well_tl(ss)
         if arity(f) = length(ss), def arity(f), def length(ss)
 Well-3 :
    Well(F(f,ss)) = false
         if arity(f) =/= length(ss), def arity(f), def length(ss)
 Well_tl-1 :
    Well_tl(nil) = true
 Well_tl-2 :
    Well_tl(cons(t,ts)) = Well_tl(ts) if
    Well(t) = true
 Well_tl-3 :
    Well_tl(cons(t,ts)) = false
    if
      Well(t) =/= true, def Well(t)
    .
call analyze-operator  Well
call analyze-operator  Well_tl
set weight s Well-def-auto
set weight ts Well_tl-def-auto
call auto-strategy :ind-lemmas { Well_tl-def-auto Well-def-auto } Well-def-auto
call auto-strategy :ind-lemmas { Well-def-auto Well_tl-def-auto } Well_tl-def-auto
call activate-lemmas { Well_tl-def-auto Well-def-auto }
assume
    { Well_tl(cons(s,ss)) = false,
      Well(s) = true }
    Well-Well_tl
call simplify  Well-Well_tl
call activate-lemma  Well-Well_tl :obl-litnbs-list { { 2 } }
assume
    { Well(F(f,ss)) = false,
      Well_tl(ss) = true }
    Well_tl-Well
call simplify Well_tl-Well
call activate-lemma  Well_tl-Well :obl-litnbs-list { { 2 } }
//assume
//    { Well(F(f,ts)) =/= true,
//      Well(F(f,ss)) =/= true,
//      length(ts) = length(ss) }
//    length-Well
//call simplify length-Well
//call activate-lemma  length-Well
declare operators
    contains_tl : Termlist VID --> Bool
    contains : Term VID --> Bool
    .
assert
 contains_tl-1 :
    contains_tl(nil,y) = false
 contains_tl-2 :
    contains_tl(cons(s,ss),y) = true
	if contains(s,y) = true
 contains_tl-3 :
    contains_tl(cons(s,ss),y) = contains_tl(ss,y)
	if contains(s,y) =/= true, def contains(s,y)
 contains-1 :
    contains(V(x),y) = true if x = y
 contains-2 :
    contains(V(x),y) = false if x =/= y
 contains-3 :
    contains(F(f,ss),y) = contains_tl(ss,y)
    .
call analyze-operator  contains
call analyze-operator  contains_tl
set weight ss contains_tl-def-auto
set weight s contains-def-auto
call auto-strategy :ind-lemmas { contains_tl-def-auto contains-def-auto } contains-def-auto
call auto-strategy :ind-lemmas { contains-def-auto contains_tl-def-auto } contains_tl-def-auto
call activate-lemmas { contains_tl-def-auto contains-def-auto }

declare operators
    Lpo : Term Term --> Bool
    Alpha : Termlist Term --> Bool
    Beta : Term Term --> Bool
    Gamma : Term Term --> Bool
    Delta : Term Term --> Bool
    Majo : Term Termlist --> Bool
    Lex : Termlist Termlist --> Bool
    .
assert
 Lpo-1 :
    Lpo(F(f,ss),F(g,ts)) = true if Alpha(ss,F(g,ts)) = true
 Lpo-2 :
    Lpo(F(f,ss),F(g,ts)) = true if Alpha(ss,F(g,ts)) =/= true, def Alpha(ss,F(g,ts)),
                                    Beta(F(f,ss),F(g,ts)) = true
 Lpo-3 :
    Lpo(F(f,ss),F(g,ts)) = Gamma(F(f,ss),F(g,ts))
       if Alpha(ss,F(g,ts)) =/= true, def Alpha(ss,F(g,ts)),
          Beta(F(f,ss),F(g,ts)) =/= true, def Beta(F(f,ss),F(g,ts))
 Lpo-4 :
    Lpo(F(f,ss),V(y)) = Delta(F(f,ss),V(y))
 Lpo-5 :
    Lpo(V(x),t) = false
 Alpha-1 :
    Alpha(nil,t) = false
 Alpha-2 :
    Alpha(cons(s,ss),t) = true if s = t
 Alpha-3 :
    Alpha(cons(s,ss),t) = true if s =/= t, Lpo(s,t) = true
 Alpha-4 :
    Alpha(cons(s,ss),t) = Alpha(ss,t) if s =/= t, Lpo(s,t) =/= true, def Lpo(s,t)
 Beta-1 :
    Beta(F(f,ss),F(g,ts)) = Majo(F(f,ss),ts) if prec(f,g) = true
 Beta-2 :
    Beta(F(f,ss),F(g,ts)) = false if prec(f,g) =/= true, def prec(f,g)
 Gamma-1 :
    Gamma(F(f,ss),F(g,ts)) = Majo(F(f,ss),ts) if f = g, Lex(ss,ts) = true
 Gamma-2 :
    Gamma(F(f,ss),F(g,ts)) = false if f =/= g
 Gamma-3 :
    Gamma(F(f,ss),F(g,ts)) = false if f = g, Lex(ss,ts) =/= true, def Lex(ss,ts)
 Delta-1 :
    Delta(F(f,ss),V(y)) = contains_tl(ss,y)
 Majo-1 :
    Majo(s,nil) = true
 Majo-2 :
    Majo(s,cons(t,ts)) = Majo(s,ts) if Lpo(s,t) = true
 Majo-3 :
    Majo(s,cons(t,ts)) = false if Lpo(s,t) =/= true, def Lpo(s,t)
 Lex-1 :
    Lex(nil,nil) = false
 Lex-2 :
    Lex(cons(s,ss),cons(t,ts)) = Lex(ss,ts) if s = t
 Lex-3 :
    Lex(cons(s,ss),cons(t,ts)) = Lpo(s,t) if s =/= t
    .

call analyze-operator  Lpo :speculate-domain-lemma-p FALSE
call analyze-operator  Alpha :speculate-domain-lemma-p FALSE
call analyze-operator  Beta :speculate-domain-lemma-p FALSE
call analyze-operator  Gamma :speculate-domain-lemma-p FALSE
call analyze-operator  Delta :speculate-domain-lemma-p FALSE
call analyze-operator  Majo :speculate-domain-lemma-p FALSE
call analyze-operator  Lex :speculate-domain-lemma-p FALSE

assume
    { def Lpo(s,t),
      Well(s) =/= true,
      Well(t) =/= true  }
    Lpo-def-manuell

assume
    { def Alpha(ss,s),
      Well_tl(ss) =/= true,
      Well(s) =/= true  }
    Alpha-def-manuell
assume
    { def Beta(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true   }
    Beta-def-manuell
assume
    { def Gamma(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    Gamma-def-manuell
assume
    { def Delta(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Var(t) =/= true   }
    Delta-def-manuell
assume
    { def Majo(s,ts),
      Well(s) =/= true,
      Well_tl(ts) =/= true }
    Majo-def-manuell
assume
    { def Lex(ss,ts),
      length(ss) =/= length(ts), 
      Well_tl(ss) =/= true, 
      Well_tl(ts) =/= true  }
    Lex-def-manuell

set weight (s,t,0) Lpo-def-manuell
set weight (ss,s) Alpha-def-manuell
set weight (s,t) Beta-def-manuell
set weight (s,t) Gamma-def-manuell
set weight (ss,ts) Lex-def-manuell
set weight (s,ts) Majo-def-manuell

call operators-strategy { 1 } { [1] } Delta-def-manuell
call activate-lemma  Delta-def-manuell

call operators-strategy { 1 } { [1] } :ind-lemmas { Alpha-def-manuell Beta-def-manuell Gamma-def-manuell } Lpo-def-manuell

call operators-strategy { 1 } { [1] } :ind-lemmas { Lpo-def-manuell Alpha-def-manuell } Alpha-def-manuell

call operators-strategy { 1 } { [1] } :ind-lemmas { Majo-def-manuell Beta-def-manuell } Beta-def-manuell

call operators-strategy { 1 } { [1] } :ind-lemmas { Majo-def-manuell Lex-def-manuell Gamma-def-manuell } Gamma-def-manuell

call operators-strategy { 1 } { [1] } :ind-lemmas { Lpo-def-manuell Majo-def-manuell } Majo-def-manuell

call operators-strategy { 1 } { [1] } :ind-lemmas { Lpo-def-manuell Lex-def-manuell } Lex-def-manuell

call activate-lemmas { Lpo-def-manuell
		       Alpha-def-manuell
		       Beta-def-manuell
    		       Gamma-def-manuell
		       Majo-def-manuell
		       Lex-def-manuell }

declare operators
    subterm : Term Term --> Bool
    subterm_tl : Term Termlist --> Bool
    .
assert subterm-1 :
    subterm(s,V(y)) = false
    .
assert subterm-2 :
    subterm(s,F(g,ts)) = subterm_tl(s,ts)
    .
assert subterm_tl-1 :
    subterm_tl(s,nil) = false
    .
assert subterm_tl-2 :
    subterm_tl(s,cons(t,ts)) = true
    if s = t
    .
assert subterm_tl-3 :
    subterm_tl(s,cons(t,ts)) = true
    if s =/= t,
       subterm(s,t) = true
    .
assert subterm_tl-4 :
    subterm_tl(s,cons(t,ts)) = subterm_tl(s,ts)
    if s =/= t,
       subterm(s,t) =/= true,
       def subterm(s,t)
    .
call analyze-operator  subterm
call analyze-operator  subterm_tl
set weight t subterm-def-auto
set weight ts subterm_tl-def-auto
call auto-strategy :ind-lemmas { subterm_tl-def-auto subterm-def-auto } subterm-def-auto
call auto-strategy :ind-lemmas { subterm-def-auto subterm_tl-def-auto } subterm_tl-def-auto
call activate-lemmas { subterm_tl-def-auto subterm-def-auto }

assume
    { subterm(s,t) = true,
      subterm(s,u) =/= true,
      subterm(u,t) =/= true }
    subterm-trans
call auto-strategy :recursive-strategy-p TRUE  subterm-trans
call activate-lemma  subterm-trans

assume
    { subterm_tl(t,cons(s,ss)) = true,
      subterm_tl(t,ss) =/= true }
    subterm_tl-cons
call simplify subterm_tl-cons
call activate-lemma  subterm_tl-cons


declare operators
    subterms : Termlist Term --> Bool
    .
assert subterms-1 :
    subterms(nil,t) = true
    .
assert subterms-2 :
    subterms(cons(s,ss),t) = subterms(ss,t)
    if subterm(s,t) = true
    .
assert subterms-3 :
    subterms(cons(s,ss),t) = false
    if subterm(s,t) =/= true,
       def subterm(s,t)
    .
call analyze-operator  subterms
call auto-strategy  subterms-def-auto
call activate-lemma  subterms-def-auto

declare operators
    subterms_tl : Termlist Termlist --> Bool
    .
assert subterms_tl-1 :
    subterms_tl(nil,ts) = true
    .
assert subterms_tl-2 :
    subterms_tl(cons(s,ss),ts) = subterms_tl(ss,ts)
    if subterm_tl(s,ts) = true
    .
assert subterms_tl-3 :
    subterms_tl(cons(s,ss),ts) = false
    if subterm_tl(s,ts) =/= true,
       def subterm_tl(s,ts)
    .
call analyze-operator  subterms_tl
call auto-strategy  subterms_tl-def-auto
call activate-lemma  subterms_tl-def-auto

assume
    { subterms_tl(ts,cons(s,ss)) = true,
      subterms_tl(ts,ss) =/= true }
    subterms_tl-cons
call auto-strategy  subterms_tl-cons
call activate-lemma  subterms_tl-cons

assume
    { subterms(ss,F(g,ts)) = true,
      subterms_tl(ss,ts) =/= true }
    subterms-subterms_tl
call auto-strategy  subterms-subterms_tl
call activate-lemma  subterms-subterms_tl

assume
    { subterms_tl(ss,ss) = true }
    subterms_tl-refl
call auto-strategy  subterms_tl-refl
call activate-lemma  subterms_tl-refl

assume
    { subterm_tl(s,ss) = false,
      subterms(ss,s) =/= true }
    subterm_tl-subterms
assume
    { subterm(s,s) = false }
    subterm-irrefl

set weight ss subterm_tl-subterms
set weight s subterm-irrefl

call auto-strategy :ind-lemmas { subterm-irrefl subterm_tl-subterms } subterm_tl-subterms
apply lemma-subs
    subterm-trans
    [s <-- t , u <-- s] ..
    subterm_tl-subterms
call simplify :ind-lemmas { subterm-irrefl } subterm_tl-subterms

call activate-ind-lemma  subterm_tl-subterms :obl-litnbs-list {  }
call auto-strategy :ind-lemmas { subterm_tl-subterms } subterm-irrefl

call activate-lemma  subterm-irrefl
//call activate-lemma  subterm_tl-subterms

declare operators
    sublist : Termlist Termlist --> Bool
    .
assert sublist-1 :
    sublist(nil,ts) = true
    .
assert sublist-2 :
    sublist(cons(s,ss),nil) = false
    .
assert sublist-3 :
    sublist(cons(s,ss),cons(t,ts)) = sublist(ss,ts)
    if s = t
    .
assert sublist-4 :
    sublist(cons(s,ss),cons(t,ts)) = sublist(cons(s,ss),ts)
    if s =/= t
    .
call analyze-operator  sublist
call auto-strategy  sublist-def-auto
call activate-lemma  sublist-def-auto

assume
    { sublist(ss,ss) = true }
    sublist-refl
call auto-strategy  sublist-refl
call activate-lemma  sublist-refl

assume
    { sublist(cons(t,ss),ts) = false,
      sublist(ss,ts) =/= false }
    sublist-cons
call auto-strategy  sublist-cons
call activate-lemma  sublist-cons

assume
    { sublist(cons(t,ss),ts) = false,
      subterm_tl(t,ts) = true }
    subterm_tl-sublist
call auto-strategy  subterm_tl-sublist
call activate-lemma  subterm_tl-sublist :obl-litnbs-list { { 2 } }

assume
    { sublist(cons(s,ss),ts) = false,
      subterms(ts,s) =/= true }
    sublist-subterms
call auto-strategy  sublist-subterms
call activate-lemma  sublist-subterms

assume
    { Lpo(s,t) = false,
      contains(s,y) = true,
      contains(t,y) =/= true,
      Well(s) =/= true,
      Well(t) =/= true  }
    contains-Lpo
assume
    { Alpha(ss,s) = false,
      contains_tl(ss,y) = true,
      contains(s,y) =/= true,
      Well_tl(ss) =/= true,
      Well(s) =/= true  }
    contains-Alpha
assume
    { Beta(s,t) = false,
      contains(s,y) = true,
      contains(t,y) =/= true,
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true   }
    contains-Beta
assume
    { Gamma(s,t) = false,
      contains(s,y) = true,
      contains(t,y) =/= true,
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true   }
    contains-Gamma
assume
    { Delta(s,t) = false,
      contains(s,y) = true,
      contains(t,y) =/= true,
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Var(t) =/= true   }
    contains-Delta
assume
    { Majo(s,ts) = false,
      contains(s,y) = true,
      contains_tl(ts,y) =/= true,
      Well(s) =/= true,
      Well_tl(ts) =/= true }
    contains-Majo
set weight (s,t,0) contains-Lpo
set weight (ss,s) contains-Alpha
set weight (s,t) contains-Beta
set weight (s,t) contains-Gamma
set weight (s,ts) contains-Majo

call operators-strategy { 1 } { [1] } contains-Delta
call activate-lemma  contains-Delta

call operators-strategy { 1 } { [1] } :ind-lemmas { contains-Alpha contains-Beta contains-Gamma contains-Lpo } contains-Lpo

call operators-strategy { 1 } { [1] } :ind-lemmas { contains-Lpo contains-Alpha } contains-Alpha

call operators-strategy { 1 } { [1] } :ind-lemmas { contains-Lpo contains-Majo contains-Beta } contains-Beta

call operators-strategy { 1 } { [1] } :ind-lemmas { contains-Lpo contains-Majo contains-Gamma } contains-Gamma

call operators-strategy { 1 } { [1] } :ind-lemmas { contains-Lpo contains-Majo } contains-Majo

call activate-lemmas { contains-Lpo
		       contains-Alpha
		       contains-Beta
		       contains-Gamma
		       contains-Majo }

assume
    { Lpo(F(f,ss),t) = true,
      Alpha(ss,t) =/= true,
      Well_tl(ss) =/= true,
      arity(f) =/= length(ss),
      Well(t) =/= true,
      Fun(t) =/= true  }
    Lpo-Alpha
call variables-strategy { t } Lpo-Alpha

assume
    { Lpo(s,t) = true,
      Beta(s,t) =/= true,
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    Lpo-Beta
call auto-strategy  Lpo-Beta

assume
    { Lpo(s,t) = true,
      Gamma(s,t) =/= true,
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    Lpo-Gamma
call auto-strategy  Lpo-Gamma

assume
    { contains(t,y) = true,
      subterm(V(y),t) =/= true }
    contains-subterm
assume
    { contains_tl(ss,y) = true,
       subterm_tl(V(y),ss) =/= true }
    contains-subterm_tl
set weight t contains-subterm
set weight ss contains-subterm_tl
call auto-strategy :ind-lemmas { contains-subterm_tl contains-subterm } contains-subterm
call auto-strategy :ind-lemmas { contains-subterm contains-subterm_tl } contains-subterm_tl
call activate-lemmas { contains-subterm contains-subterm_tl }

assume
    { Lpo(t,s) = true,
      subterm(s,t) =/= true,
      Well(s) =/= true,
      Well(t) =/= true }
    Lpo-subterm
assume
    { Alpha(ts,s) = true,
      subterm_tl(s,ts) =/= true,
      Well(s) =/= true,
      Well_tl(ts) =/= true }
    Alpha-subterm_tl
set weight t Lpo-subterm
set weight ts Alpha-subterm_tl

call variables-strategy  { t s } :ind-lemmas { Alpha-subterm_tl } Lpo-subterm
call auto-strategy :ind-lemmas { Lpo-subterm Alpha-subterm_tl } Alpha-subterm_tl

call activate-lemma  Alpha-subterm_tl

assume
    { Lpo(F(g,ts),s) = true,
      subterm_tl(s,ts) =/= true,
      Well(s) =/= true,
      Well_tl(ts) =/= true,
      arity(g) =/= length(ts) }
    Lpo-subterm_tl
call variables-strategy  { s } Lpo-subterm_tl
call activate-lemma  Lpo-subterm_tl

assume
    { Lpo(s,u) =/= true,
      Lpo(u,t) =/= true,
      Lpo(s,t) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well(u) =/= true }
    Lpo-trans
assume
    { Alpha(ss,F(h,us)) =/= true,
      Alpha(us,t) =/= true,
      Alpha(ss,t) = true,
      Well_tl(ss) =/= true,
      Well(t) =/= true,
      Well_tl(us) =/= true,
      arity(h) =/= length(us),
      Fun(t) =/= true }
    Alpha-Alpha-trans
assume
    { Alpha(ss,u) =/= true,
      Beta(u,t) =/= true,
      Alpha(ss,t) = true,
      Well_tl(ss) =/= true,
      Well(t) =/= true,
      Well(u) =/= true,
      Fun(t) =/= true,
      Fun(u) =/= true }
    Alpha-Beta-trans
assume
    { Alpha(ss,u) =/= true,
      Gamma(u,t) =/= true,
      Alpha(ss,t) = true,
      Well_tl(ss) =/= true,
      Well(t) =/= true,
      Well(u) =/= true,
      Fun(t) =/= true,
      Fun(u) =/= true }
    Alpha-Gamma-trans
assume
    { Beta(s,F(h,us)) =/= true,
      Alpha(us,t) =/= true,
      Lpo(s,t) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well_tl(us) =/= true,
      arity(h) =/= length(us),
      Fun(s) =/= true,
      Fun(t) =/= true  }
    Beta-Alpha-trans
assume
    { Beta(s,u) =/= true,
      Beta(u,t) =/= true,
      Beta(s,t) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well(u) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true,
      Fun(u) =/= true  }
    Beta-Beta-trans
assume
    { Beta(s,u) =/= true,
      Gamma(u,t) =/= true,
      Beta(s,t) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well(u) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true,
      Fun(u) =/= true  }
    Beta-Gamma-trans
assume
    { Gamma(s,F(h,us)) =/= true,
      Alpha(us,t) =/= true,
      Lpo(s,t) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well_tl(us) =/= true,
      arity(h) =/= length(us),
      Fun(s) =/= true,
      Fun(t) =/= true  }
    Gamma-Alpha-trans
assume
    { Gamma(s,u) =/= true,
      Beta(u,t) =/= true,
      Beta(s,t) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well(u) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true,
      Fun(u) =/= true  }
    Gamma-Beta-trans
assume
    { Gamma(s,u) =/= true,
      Gamma(u,t) =/= true,
      Gamma(s,t) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well(u) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true,
      Fun(u) =/= true  }
    Gamma-Gamma-trans
assume
    { Majo(s,us) =/= true,
      Alpha(us,t) =/= true,
      Lpo(s,t) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well_tl(us) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    Majo-Alpha-trans
assume
    { Majo(F(f,ss),ts) =/= true,
      Majo(F(g,ts),us) =/= true,
      Majo(F(f,ss),us) = true,
      prec(f,g) =/= true,
      Well_tl(ss) =/= true,
      arity(f) =/= length(ss),
      Well_tl(ts) =/= true,
      arity(g) =/= length(ts),
      Well_tl(us) =/= true }
    Majo-Majo-trans
assume
    { Majo(F(g,ss),ts) =/= true,
      Majo(F(g,ts),us) =/= true,
      Majo(F(g,ss),us) = true,
      Lex(ss,ts) =/= true,
      Well_tl(ss) =/= true,
      arity(g) =/= length(ss),
      Well_tl(ts) =/= true,
      arity(g) =/= length(ts),
      Well_tl(us) =/= true }
    Majo-Majo-Lex-trans
assume
    { Lex(ss,ts) =/= true,
      Lex(ts,us) =/= true,
      Lex(ss,us) = true,
      length(ss) =/= length(ts),
      length(ts) =/= length(us),
      Well_tl(ss) =/= true,
      Well_tl(us) =/= true,
      Well_tl(ts) =/= true }
    Lex-Lex-trans
assume
    { Alpha(ss,t) =/= true,
      Delta(t,V(y)) =/= true,
      Delta(F(f,ss),V(y)) = true,
      Well_tl(ss) =/= true,
      arity(f) =/= length(ss),
      Well(t) =/= true,
      Well(V(y)) =/= true,
      Fun(t) =/= true }
    Alpha-Delta-trans
assume
    { Beta(s,t) =/= true,
      Delta(t,V(y)) =/= true,
      Delta(s,V(y)) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well(V(y)) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    Beta-Delta-trans
assume
    { Gamma(s,t) =/= true,
      Delta(t,V(y)) =/= true,
      Delta(s,V(y)) = true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well(V(y)) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    Gamma-Delta-trans

assume
    { Lpo(s,s) = false,
      Well(s) =/= true }
    Lpo-irrefl
assume
    { Alpha(ss,F(g,ts)) = false,
      sublist(ss,ts) =/= true,
      Well_tl(ts) =/= true,
      arity(g) =/= length(ts),
      Well_tl(ss) =/= true }
    Alpha-irrefl
assume
    { Beta(s,s) = false,
      Well(s) =/= true,
      Fun(s) =/= true }
    Beta-irrefl
assume
    { Gamma(s,s) = false,
      Well(s) =/= true,
      Fun(s) =/= true }
    Gamma-irrefl
assume
    { Lex(ss,ss) = false,
      Well_tl(ss) =/= true }
    Lex-irrefl

call set-default-settings :activate-first-lit-p TRUE

call auto-strategy  Beta-irrefl
call activate-lemma  Beta-irrefl

call auto-strategy  Lex-irrefl
call activate-lemma  Lex-irrefl

call auto-strategy  Gamma-irrefl
call activate-lemma  Gamma-irrefl

call simplify  Alpha-Delta-trans
call activate-lemma  Alpha-Delta-trans

call operators-strategy { 1 } { [1] } Beta-Delta-trans
call activate-lemma  Beta-Delta-trans

call operators-strategy { 1 } { [1] } Gamma-Delta-trans
call activate-lemma  Gamma-Delta-trans

set weight (s,t,u,0) Lpo-trans
set weight ss Alpha-Alpha-trans
set weight ss Alpha-Beta-trans
set weight ss Alpha-Gamma-trans
set weight (s,t,us,0) Beta-Alpha-trans
set weight (s,t,u) Beta-Beta-trans
set weight (s,t,u) Beta-Gamma-trans
set weight (s,t,us,0) Gamma-Alpha-trans
set weight (s,t,u) Gamma-Beta-trans
set weight (s,t,u) Gamma-Gamma-trans
set weight (s,t,us) Majo-Alpha-trans
set weight (F(f,ss),us,ts) Majo-Majo-trans
set weight (F(g,ss),us,ts) Majo-Majo-Lex-trans
set weight (ss,us,ts) Lex-Lex-trans
set weight s Lpo-irrefl
set weight ss Alpha-irrefl

call deactivate-axioms  { Alpha-1 Alpha-2 Alpha-3 Alpha-4 Beta-1 Beta-2 Gamma-1 Gamma-2 Gamma-3 Delta-1 }
call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Alpha-Alpha-trans Alpha-Beta-trans Alpha-Gamma-trans Beta-Alpha-trans Beta-Beta-trans Beta-Gamma-trans Gamma-Alpha-trans Gamma-Beta-trans Gamma-Gamma-trans Lpo-trans } Lpo-trans
call activate-axioms  { Delta-1 Gamma-3 Gamma-2 Gamma-1 Beta-2 Beta-1 Alpha-4 Alpha-3 Alpha-2 Alpha-1 }

call activate-lemma  Lpo-Alpha
call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Lpo-trans Alpha-Alpha-trans } Alpha-Alpha-trans
call deactivate-lemmas { Lpo-Alpha }

call activate-lemma  Lpo-Beta
call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Lpo-trans Alpha-Beta-trans } Alpha-Beta-trans
call deactivate-lemmas { Lpo-Beta }

call activate-lemma  Lpo-Gamma
call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Lpo-trans Alpha-Gamma-trans } Alpha-Gamma-trans
call deactivate-lemmas { Lpo-Gamma }

call variables-strategy { s } :ind-lemmas { Majo-Alpha-trans } Beta-Alpha-trans

call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Majo-Majo-trans Beta-Beta-trans } Beta-Beta-trans

call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Majo-Majo-trans Beta-Gamma-trans } Beta-Gamma-trans

call variables-strategy { s } :ind-lemmas { Majo-Alpha-trans } Gamma-Alpha-trans

call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Majo-Majo-Lex-trans Gamma-Beta-trans } Gamma-Beta-trans

call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Majo-Majo-Lex-trans Lex-Lex-trans Gamma-Gamma-trans } Gamma-Gamma-trans

call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Lpo-trans Majo-Alpha-trans } Majo-Alpha-trans

call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Lpo-trans Majo-Majo-trans } Majo-Majo-trans
apply ind-subs
    Lpo-trans
    [s<--F(f,ss),u <-- F(g,ts) , t <-- t] ..
    Majo-Majo-trans
call cont-proof-attempt :ind-lemmas { Majo-Majo-trans } Majo-Majo-trans

call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Lpo-trans Majo-Majo-Lex-trans } Majo-Majo-Lex-trans
apply ind-subs
    Lpo-trans
    [s <-- F(g,ss) , t <-- t, u<--F(g,ts)] ..
    Majo-Majo-Lex-trans
call cont-proof-attempt :ind-lemmas { Majo-Majo-Lex-trans } Majo-Majo-Lex-trans

call activate-lemma  Lpo-subterm
call operators-strategy  { 1 2 } { [1] [1] } :ind-lemmas { Lpo-trans Lpo-irrefl Lex-Lex-trans } Lex-Lex-trans
call deactivate-lemmas { Lpo-subterm }

call auto-strategy :ind-lemmas { Alpha-irrefl Lpo-irrefl } Lpo-irrefl

call auto-strategy  Alpha-irrefl
apply lemma-rewrite
    4
    [1]
    subterm_tl-sublist
    1
    [t <-- t , ss <-- ss , ts <-- ts] ..
    Alpha-irrefl
apply ind-subs
    Lpo-trans
    [s <-- t , u <-- F(g,ts)] ..
    Alpha-irrefl
call activate-lemma  Lpo-subterm
call cont-proof-attempt :ind-lemmas { Lpo-irrefl } Alpha-irrefl
call deactivate-lemmas { Lpo-subterm }

call activate-lemma  Lpo-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Alpha-Alpha-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Alpha-Beta-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Alpha-Gamma-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Beta-Alpha-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Beta-Beta-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Beta-Gamma-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Gamma-Alpha-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Gamma-Beta-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Gamma-Gamma-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Majo-Alpha-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Majo-Majo-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Majo-Majo-Lex-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemma  Lex-Lex-trans :head-litnbs { 3 } :obl-litnbs-list { { 1 } { 2 } }
call activate-lemmas  { Alpha-irrefl Lpo-irrefl }

call set-default-settings :activate-first-lit-p FALSE

assume
    { gt-nat(n,0) = true,
      n = 0 }
    gt-nat-0
call auto-strategy  gt-nat-0
call activate-lemma  gt-nat-0

assume
    { gt-nat(S(0),n) = false,
      n = 0 }
    gt-nat-S0
call auto-strategy  gt-nat-S0
call activate-lemma  gt-nat-S0

assume
    { gt-nat(S(m),n) = true,
      gt-nat(n,m) = true }
    gt-nat-complete
call auto-strategy  gt-nat-complete
call activate-lemma  gt-nat-complete

declare operators
    term-arg_tl : Termlist Nat --> Term
    .
assert term-arg_tl-1 :
    term-arg_tl(cons(s,ss),S(0)) = s
    .
assert term-arg_tl-2 :
    term-arg_tl(cons(s,ss),S(S(n))) = term-arg_tl(ss,S(n))
    .

call analyze-operator  term-arg_tl
assume
    { def term-arg_tl(ss,n),
      n = 0,
      gt-nat(n,length(ss)) = true }
    def-term-arg_tl
call operators-strategy  { 1 } { [1] } def-term-arg_tl
call activate-lemma  def-term-arg_tl

declare sorts Natlist.

define sort Natlist with constructors
    nnil :  --> Natlist
    ncons : Nat Natlist --> Natlist
    .

declare constructor variables l : Natlist.

declare operators
    pos-p : Natlist Term --> Bool
    .
assert pos-p-1 :
    pos-p(nnil,s) = true
    .
assert pos-p-2 :
    pos-p(ncons(n,l),V(x)) = false
    .
assert pos-p-3 :
    pos-p(ncons(n,l),F(f,ss)) = false
    if n = 0
    .
assert pos-p-4 :
    pos-p(ncons(n,l),F(f,ss)) = false
    if
      n =/= 0,
      gt-nat(n,length(ss)) = true
    .
assert pos-p-5 :
    pos-p(ncons(n,l),F(f,ss)) = pos-p(l,term-arg_tl(ss,n))
    if n =/= 0,
       gt-nat(n,length(ss)) =/= true,
       def gt-nat(n,length(ss))
    .

call analyze-operator  pos-p
call auto-strategy  pos-p-def-auto
call activate-lemma  pos-p-def-auto

declare operators
    replace : Term Natlist Term --> Term
    .
declare operators
    replace_tl : Termlist Nat Natlist Term --> Termlist
    .
assert replace-1 :
    replace(s,nnil,t) = t
    .
assert replace-2 :
    replace(F(f,ss),ncons(n,l),t) = F(f,replace_tl(ss,n,l,t))
    .
assert replace_tl-1 :
    replace_tl(cons(s,ss),S(0),l,t) = cons(replace(s,l,t),ss)
    .
assert replace_tl-2 :
    replace_tl(cons(s,ss),S(S(n)),l,t) = cons(s,replace_tl(ss,S(n),l,t))
    .

declare operators
    elem : Term Termlist --> Bool
    .
assert elem-1 :
    elem(s,nil) = false
    .
assert elem-2 :
    elem(s,cons(t,ts)) = true
    if
      s = t
    .
assert elem-3 :
    elem(s,cons(t,ts)) = elem(s,ts)
    if
      s =/= t
    .

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

assume
    { sublist(cons(s,ss),ts) = false,
      elem(s,ts) = true }
    elem-sublist
call auto-strategy  elem-sublist
call activate-lemma  elem-sublist

assume
    { subterm_tl(t,ss) = true,
      elem(t,ss) =/= true }
    subterm_tl-elem
call auto-strategy  subterm_tl-elem
call activate-lemma  subterm_tl-elem

assume
    { subterm(t,F(f,ss)) = true,
      elem(t,ss) =/= true }
    subterm-elem
call simplify  subterm-elem
call activate-lemma  subterm-elem

declare operators
    replace1_tl : Termlist Nat Term --> Termlist
    .
assert replace1_tl-1 :
    replace1_tl(cons(s,ss),S(0),t) = cons(t,ss)
    .
assert replace1_tl-2 :
    replace1_tl(cons(s,ss),S(S(n)),t) = cons(s,replace1_tl(ss,S(n),t))
    .

call analyze-operator  replace1_tl
assume
    { def replace1_tl(ss,n,t),
      n = 0,
      gt-nat(S(length(ss)),n) =/= true }
    def-replace1_tl
call operators-strategy  { 1 } { [1] }  def-replace1_tl
call activate-lemma  def-replace1_tl

assume
    { Well_tl(replace1_tl(ss,n,t)) = Well(t),
      Well_tl(ss) =/= true,
      n = 0,
      gt-nat(S(length(ss)),n) =/= true }
    Well_tl-replace1_tl
call operators-strategy  { 1 } { [1:1] } Well_tl-replace1_tl
call activate-lemma  Well_tl-replace1_tl

assume
    { replace1_tl(ss,n,t) =/= replace1_tl(ss,n,u),
      n = 0,
      gt-nat(S(length(ss)),n) =/= true,
      t = u }
    replace1_tl-id
call operators-strategy  { 1 1 } { [1] [2] } replace1_tl-id
call activate-lemma  replace1_tl-id

assume
    { length(replace1_tl(ss,n,t)) = length(ss),
      n = 0,
      gt-nat(S(length(ss)),n) =/= true }
    length-replace1_tl
call operators-strategy  { 1 } { [1:1] } length-replace1_tl
call activate-lemma  length-replace1_tl

assume
    { elem(s,replace1_tl(ss,n,t)) = true,
      elem(s,replace1_tl(ss,n,u)) =/= true,
      s = u,
      n = 0,
      gt-nat(n,length(ss)) = true }
    elem-replace1_tl
call operators-strategy  { 1 2 } { [1:2] [1:2] } elem-replace1_tl
call activate-lemma  elem-replace1_tl

assume
    { elem(t,replace1_tl(ss,n,t)) = true,
      n = 0,
      gt-nat(n,length(ss)) = true }
    elem-replace1_tl-1
call operators-strategy  { 1 } { [1:2] } elem-replace1_tl-1
call activate-lemma  elem-replace1_tl-1

assume
    { sublist(cons(s,ts),replace1_tl(ss,n,u)) =/= true,
      elem(s,replace1_tl(ss,n,t)) = true,
      s = u,
      n = 0,
      gt-nat(n,length(ss)) = true }
    elem-sublist-replace1_tl
call simplify  elem-sublist-replace1_tl
call activate-lemma  elem-sublist-replace1_tl

assume
    { Lex(replace1_tl(ss,n,t),replace1_tl(ss,n,u)) = true,
      Lpo(t,u) =/= true,
      Well_tl(ss) =/= true,
      Well(t) =/= true,
      Well(u) =/= true,
      n = 0,
      gt-nat(n,length(ss)) = true }
    Lex-replace1_tl
call operators-strategy  { 1 1 } { [1:1] [1:2] }  Lex-replace1_tl
call activate-lemma  Lex-replace1_tl

call activate-lemma  Lpo-subterm :head-litnbs { 1 } :obl-litnbs-list {  }
call activate-lemma  subterm_tl-elem :head-litnbs { 1 } :obl-litnbs-list {  }
assume
    { Majo(F(f,replace1_tl(ss,n,t)),ts) = true,
      sublist(ts,replace1_tl(ss,n,u)) =/= true,
      Lpo(t,u) =/= true,
      Well_tl(ss) =/= true,
      arity(f) =/= length(ss),
      Well_tl(ts) =/= true,
      Well(t) =/= true,
      n = 0,
      gt-nat(n,length(ss)) = true }
    Majo-replace1_tl
call auto-strategy  Majo-replace1_tl
call activate-lemma  Majo-replace1_tl
call activate-lemma  Lpo-subterm
call activate-lemma  subterm_tl-elem

assume
    { Gamma(F(f,replace1_tl(ss,n,t)),F(f,replace1_tl(ss,n,u))) = true,
      Lpo(t,u) =/= true,
      Well_tl(ss) =/= true,
      arity(f) =/= length(ss),
      Well(t) =/= true,
      Well(u) =/= true,
      n = 0,
      gt-nat(n,length(ss)) = true }
    Gamma-replace1_tl
call simplify  Gamma-replace1_tl
call activate-lemma  Gamma-replace1_tl

assume
    { Lpo(F(f,replace1_tl(ss,n,t)),F(f,replace1_tl(ss,n,u))) = true,
      Lpo(t,u) =/= true,
      Well_tl(ss) =/= true,
      arity(f) =/= length(ss),
      Well(t) =/= true,
      Well(u) =/= true,
      n = 0,
      gt-nat(n,length(ss)) = true }
    Lpo-replace1_tl
call simplify  Lpo-replace1_tl
call activate-lemma  Lpo-replace1_tl

assume
    { Well(term-arg_tl(ss,n)) = true,
      Well_tl(ss) =/= true,
      n = 0,
      gt-nat(n,length(ss)) = true }
    Well-term-arg_tl
call auto-strategy  Well-term-arg_tl
call activate-lemma  Well-term-arg_tl

call analyze-operator  replace
call analyze-operator  replace_tl
assume
    { def replace(s,l,t),
      Well(s) =/= true,
      pos-p(l,s) =/= true }
    def-replace
assume
    { def replace_tl(ss,n,l,t),
      Well_tl(ss) =/= true,
      n = 0,
      gt-nat(S(length(ss)),n) =/= true,
      pos-p(l,term-arg_tl(ss,n)) =/= true }
    def-replace_tl

set weight s def-replace
set weight ss def-replace_tl

call operators-strategy  { 1 } { [1] } :ind-lemmas { def-replace_tl def-replace } def-replace
call operators-strategy  { 1 } { [1] } :ind-lemmas { def-replace def-replace_tl } def-replace_tl
call activate-lemmas  { def-replace def-replace_tl }

assume
    { length(replace_tl(ss,n,l,t)) = length(ss),
      Well_tl(ss) =/= true,
      n = 0,
      gt-nat(S(length(ss)),n) =/= true,
      pos-p(l,term-arg_tl(ss,n)) =/= true }
    length-replace_tl
call operators-strategy  { 1 } { [1:1] } length-replace_tl
call activate-lemma  length-replace_tl

assume
    { Well(replace(s,l,t)) = Well(t),
      Well(s) =/= true,
      pos-p(l,s) =/= true }
    Well-replace
assume
    { Well_tl(replace_tl(ss,n,l,t)) = Well(t),
      Well_tl(ss) =/= true,
      n = 0,
      gt-nat(S(length(ss)),n) =/= true,
      pos-p(l,term-arg_tl(ss,n)) =/= true }
    Well_tl-replace_tl
set weight s Well-replace
set weight ss Well_tl-replace_tl
call operators-strategy  { 1 } { [1:1] } :ind-lemmas { Well_tl-replace_tl Well-replace } Well-replace
call operators-strategy  { 1 } { [1:1] } :ind-lemmas { Well-replace Well_tl-replace_tl } Well_tl-replace_tl
call activate-lemmas  { Well-replace Well_tl-replace_tl }

// assume
//     { replace(s,l,t) =/= replace(s,l,u),
//       Well(s) =/= true,
//       pos-p(l,s) =/= true,
//       t = u }
//     replace-id
// assume
//     { replace_tl(ss,n,l,t) =/= replace_tl(ss,n,l,u),
//       Well_tl(ss) =/= true,
//       n = 0,
//       gt-nat(S(length(ss)),n) =/= true,
//       pos-p(l,term-arg_tl(ss,n)) =/= true,
//       t = u }
//     replace_tl-id
// set weight s replace-id
// set weight ss replace_tl-id
// call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { replace_tl-id replace-id } replace-id
// call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { replace-id replace_tl-id } replace_tl-id
// call activate-lemmas  { replace-id replace_tl-id }

// assume
//     { elem(s,replace_tl(ss,n,l,t)) = true,
//       elem(s,replace_tl(ss,n,l,u)) =/= true,
//       s = replace(term-arg_tl(ss,n),l,u),
//       Well(s) =/= true,
//       Well_tl(ss) =/= true,
//       Well(t) =/= true,
//       Well(u) =/= true,
//       n = 0,
//       gt-nat(n,length(ss)) = true,
//       pos-p(l,term-arg_tl(ss,n)) =/= true }
//     elem-replace_tl
// call operators-strategy  { 1 2 } { [1:2] [1:2] } elem-replace_tl
// call activate-lemma  elem-replace_tl :head-litnbs { 1 2 }

assume
    { replace_tl(ss,n,l,t) = replace1_tl(ss,n,replace(term-arg_tl(ss,n),l,t)),
      Well_tl(ss) =/= true,
      Well(t) =/= true,
      n = 0,
      gt-nat(n,length(ss)) = true,
      pos-p(l,term-arg_tl(ss,n)) =/= true }
    replace_tl-replace1_tl
call operators-strategy  { 1 1 } { [1] [2] }  replace_tl-replace1_tl
call activate-lemma  replace_tl-replace1_tl :head-litnbs { 1 } :obl-litnbs-list {  }

assume
    { Lpo(replace(s,l,t),replace(s,l,u)) =  true,
      Lpo(t,u) =/= true,
      Well(s) =/= true,
      Well(t) =/= true,
      Well(u) =/= true,
      pos-p(l,s) =/= true }
    Lpo-replace
call deactivate-axioms  { Lpo-1 Lpo-2 Lpo-3 Lpo-4 Lpo-5 }
call operators-strategy  { 1 1 } { [1:1] [1:2] }  Lpo-replace
call activate-axioms  { Lpo-5 Lpo-4 Lpo-3 Lpo-2 Lpo-1 }
call activate-lemma  Lpo-replace

// assume
//     { Gamma(F(f,replace_tl(ss,n,l,t)),F(f,replace_tl(ss,n,l,u))) = true,
//       Lpo(t,u) =/= true,
//       Well(F(f,ss)) =/= true,
//       Well(t) =/= true,
//       Well(u) =/= true,
//       n = 0,
//       gt-nat(n,length(ss)) = true,
//       pos-p(l,term-arg_tl(ss,n)) =/= true }
//     Gamma-replace_tl

// assume
//     { Majo(F(f,replace_tl(ss,n,l,t)),ts) = true,
//       sublist(ts,replace_tl(ss,n,l,u)) =/= true,
//       Lpo(t,u) =/= true,
//       Well(F(f,ss)) =/= true,
//       Well_tl(ts) =/= true,
//       Well(t) =/= true,
//       Well(u) =/= true,
//       n = 0,
//       gt-nat(n,length(ss)) = true,
//       pos-p(l,term-arg_tl(ss,n)) =/= true }
//     Majo-replace_tl

// assume
//     { Lex(replace_tl(ss,n,l,t),replace_tl(ss,n,l,u)) = true,
//       Lpo(t,u) =/= true,
//       Well_tl(ss) =/= true,
//       Well(t) =/= true,
//       Well(u) =/= true,
//       n = 0,
//       gt-nat(n,length(ss)) = true,
//       pos-p(l,term-arg_tl(ss,n)) =/= true }
//     Lex-replace_tl

declare operators
    lpo1 : Term Term --> Bool
    alpha1 : Termlist Term --> Bool
    beta1 : Term Term --> Bool
    gamma1 : Term Term --> Bool
    delta1 : Term Term --> Bool
    majo1 : Term Termlist --> Bool
    lex1 : Termlist Termlist --> Bool
    .

assert lex1-1 :
    lex1(nil,nil) = false
    .
assert lex1-2 :
    lex1(cons(s,ss),cons(t,ts)) = lex1(ss,ts)
      if s = t
    .
assert lex1-3 :
    lex1(cons(s,ss),cons(t,ts)) = lpo1(s,t)
    if s =/= t
    .

assert majo1-1 :
    majo1(s,nil) = true
    .
assert majo1-2 :
    majo1(s,cons(t,ts)) = and(lpo1(s,t),majo1(s,ts))
    .

assert delta1-1 :
    delta1(F(f,ss),V(y)) = contains_tl(ss,y)
    .

assert gamma1-1 :
    gamma1(F(f,ss),F(g,ts)) = and(lex1(ss,ts),majo1(F(f,ss),ts))
      if f = g
    .
assert gamma1-2 :
    gamma1(F(f,ss),F(g,ts)) = false
    if
      f =/= g
    .

assert beta1-1 :
    beta1(F(f,ss),F(g,ts)) = and(prec(f,g),majo1(F(f,ss),ts))
    .

assert alpha1-1 :
    alpha1(nil,t) = false
    .
assert alpha1-2 :
    alpha1(cons(s,ss),t) = true
    if
      s = t
    .
assert alpha1-3 :
    alpha1(cons(s,ss),t) = or(lpo1(s,t),alpha1(ss,t))
    if
      s =/= t
    .

assert lpo1-1 :
    lpo1(V(x),t) = false
    .
assert lpo1-2 :
    lpo1(F(f,ss),V(y)) = delta1(F(f,ss),V(y))
    .
assert lpo1-3 :
    lpo1(F(f,ss),F(g,ts)) = or(alpha1(ss,F(g,ts)),or(beta1(F(f,ss),F(g,ts)),gamma1(F(f,ss),F(g,ts))))
    .

call analyze-operator  lpo1 :speculate-domain-lemma-p FALSE
call analyze-operator  alpha1 :speculate-domain-lemma-p FALSE
call analyze-operator  beta1 :speculate-domain-lemma-p FALSE
call analyze-operator  gamma1 :speculate-domain-lemma-p FALSE
call analyze-operator  delta1 :speculate-domain-lemma-p FALSE
call analyze-operator  majo1 :speculate-domain-lemma-p FALSE
call analyze-operator  lex1 :speculate-domain-lemma-p FALSE

assume
    { def lpo1(s,t),
      Well(s) =/= true,
      Well(t) =/= true  }
    lpo1-def-manuell
assume
    { def alpha1(ss,s),
      Well_tl(ss) =/= true,
      Well(s) =/= true  }
    alpha1-def-manuell
assume
    { def beta1(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true   }
    beta1-def-manuell
assume
    { def gamma1(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    gamma1-def-manuell
assume
    { def delta1(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Var(t) =/= true   }
    delta1-def-manuell
assume
    { def majo1(s,ts),
      Well(s) =/= true,
      Well_tl(ts) =/= true }
    majo1-def-manuell
assume
    { def lex1(ss,ts),
      length(ss) =/= length(ts), 
      Well_tl(ss) =/= true, 
      Well_tl(ts) =/= true  }
    lex1-def-manuell

set weight (s,t,0) lpo1-def-manuell
set weight (ss,s) alpha1-def-manuell
set weight (s,t) beta1-def-manuell
set weight (s,t) gamma1-def-manuell
set weight (ss,ts) lex1-def-manuell
set weight (s,ts) majo1-def-manuell

call operators-strategy { 1 } { [1] } delta1-def-manuell
call activate-lemma  delta1-def-manuell

call operators-strategy { 1 } { [1] } :ind-lemmas { alpha1-def-manuell beta1-def-manuell gamma1-def-manuell majo1-def-manuell lex1-def-manuell } lpo1-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { lpo1-def-manuell alpha1-def-manuell } alpha1-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { majo1-def-manuell beta1-def-manuell } beta1-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { majo1-def-manuell lex1-def-manuell gamma1-def-manuell } gamma1-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { lpo1-def-manuell majo1-def-manuell } majo1-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { lpo1-def-manuell lex1-def-manuell } lex1-def-manuell

call activate-lemmas { lpo1-def-manuell
		       alpha1-def-manuell
		       beta1-def-manuell
    		       gamma1-def-manuell
		       majo1-def-manuell
		       lex1-def-manuell }

assume
    { lpo1(s,t) = Lpo(s,t),
      Well(s) =/= true,
      Well(t) =/= true  }
    lpo1-Lpo
assume
    { alpha1(ss,s) = Alpha(ss,s),
      Well_tl(ss) =/= true,
      Well(s) =/= true  }
    alpha1-Alpha
assume
    { beta1(s,t) = Beta(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true   }
    beta1-Beta
assume
    { gamma1(s,t) = Gamma(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    gamma1-Gamma
assume
    { delta1(s,t) = Delta(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Var(t) =/= true   }
    delta1-Delta
assume
    { majo1(s,ts) = Majo(s,ts),
      Well(s) =/= true,
      Well_tl(ts) =/= true }
    majo1-Majo
assume
    { lex1(ss,ts) = Lex(ss,ts),
      length(ss) =/= length(ts),
      Well_tl(ss) =/= true,
      Well_tl(ts) =/= true }
    lex1-Lex

set weight (s,t,0) lpo1-Lpo
set weight (ss,s) alpha1-Alpha
set weight (s,t) beta1-Beta
set weight (s,t) gamma1-Gamma
set weight (ss,ts) lex1-Lex
set weight (s,ts) majo1-Majo

call operators-strategy { 1 } { [1] } delta1-Delta
call activate-lemma  delta1-Delta :obl-litnbs-list { }

call deactivate-axioms  { Alpha-1 Alpha-2 Alpha-3 Alpha-4 Beta-1 Beta-2 Gamma-1 Gamma-2 Gamma-3 Delta-1 delta1-1 gamma1-1 gamma1-2 beta1-1 alpha1-1 alpha1-2 alpha1-3 }
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { alpha1-Alpha beta1-Beta gamma1-Gamma } lpo1-Lpo
call activate-axioms  { alpha1-3 alpha1-2 alpha1-1 beta1-1 gamma1-2 gamma1-1 delta1-1 Delta-1 Gamma-3 Gamma-2 Gamma-1 Beta-2 Beta-1 Alpha-4 Alpha-3 Alpha-2 Alpha-1 }
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { alpha1-Alpha lpo1-Lpo } alpha1-Alpha
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { beta1-Beta majo1-Majo } beta1-Beta
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { majo1-Majo lex1-Lex gamma1-Gamma } gamma1-Gamma
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { majo1-Majo lpo1-Lpo } majo1-Majo
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { lpo1-Lpo lex1-Lex } lex1-Lex

call activate-lemma  lpo1-Lpo :obl-litnbs-list { }
call activate-lemma  alpha1-Alpha :obl-litnbs-list { }
call activate-lemma  beta1-Beta :obl-litnbs-list { }
call activate-lemma  gamma1-Gamma :obl-litnbs-list { }
call activate-lemma  majo1-Majo :obl-litnbs-list { }
call activate-lemma  lex1-Lex :obl-litnbs-list { }

declare operators
    lpo2 : Term Term --> Bool
    alpha2 : Termlist Term --> Bool
    beta2 : Term Term --> Bool
    gamma2 : Term Term --> Bool
    delta2 : Term Term --> Bool
    majo2 : Term Termlist --> Bool
    lex2 : Termlist Termlist --> Bool
    .

assert lex2-1 :
    lex2(nil,nil) = false
    .
assert lex2-2 :
    lex2(cons(s,ss),cons(t,ts)) = lex2(ss,ts)
      if s = t
    .
assert lex2-3 :
    lex2(cons(s,ss),cons(t,ts)) = lpo2(s,t)
    if s =/= t
    .

assert majo2-1 :
    majo2(s,nil) = true
    .
assert majo2-2 :
    majo2(s,cons(t,ts)) = and(lpo2(s,t),majo2(s,ts))
    .

assert delta2-1 :
    delta2(F(f,ss),V(y)) = contains_tl(ss,y)
    .

assert gamma2-1 :
    gamma2(F(f,ss),F(g,ts)) = and(lex2(ss,ts),majo2(F(f,ss),ts))
      if f = g
    .
assert gamma2-2 :
    gamma2(F(f,ss),F(g,ts)) = false
    if
      f =/= g
    .

assert beta2-1 :
    beta2(F(f,ss),F(g,ts)) = and(prec(f,g),majo2(F(f,ss),ts))
    .

assert alpha2-1 :
    alpha2(nil,t) = false
    .
assert alpha2-2 :
    alpha2(cons(s,ss),t) = true
    if
      s = t
    .
assert alpha2-3 :
    alpha2(cons(s,ss),t) = or(lpo2(s,t),alpha2(ss,t))
    if
      s =/= t
    .

assert lpo2-1 :
    lpo2(V(x),t) = false
    .
assert lpo2-2 :
    lpo2(F(f,ss),V(y)) = delta2(F(f,ss),V(y))
    .
assert lpo2-3 :
    lpo2(F(f,ss),F(g,ts)) = or(beta2(F(f,ss),F(g,ts)),or(gamma2(F(f,ss),F(g,ts)),alpha2(ss,F(g,ts))))
    .

call analyze-operator  lpo2 :speculate-domain-lemma-p FALSE
call analyze-operator  alpha2 :speculate-domain-lemma-p FALSE
call analyze-operator  beta2 :speculate-domain-lemma-p FALSE
call analyze-operator  gamma2 :speculate-domain-lemma-p FALSE
call analyze-operator  delta2 :speculate-domain-lemma-p FALSE
call analyze-operator  majo2 :speculate-domain-lemma-p FALSE
call analyze-operator  lex2 :speculate-domain-lemma-p FALSE

assume
    { def lpo2(s,t),
      Well(s) =/= true,
      Well(t) =/= true  }
    lpo2-def-manuell
assume
    { def alpha2(ss,s),
      Well_tl(ss) =/= true,
      Well(s) =/= true  }
    alpha2-def-manuell
assume
    { def beta2(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true   }
    beta2-def-manuell
assume
    { def gamma2(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    gamma2-def-manuell
assume
    { def delta2(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Var(t) =/= true   }
    delta2-def-manuell
assume
    { def majo2(s,ts),
      Well(s) =/= true,
      Well_tl(ts) =/= true }
    majo2-def-manuell
assume
    { def lex2(ss,ts),
      length(ss) =/= length(ts), 
      Well_tl(ss) =/= true, 
      Well_tl(ts) =/= true  }
    lex2-def-manuell

set weight (s,t,0) lpo2-def-manuell
set weight (ss,s) alpha2-def-manuell
set weight (s,t) beta2-def-manuell
set weight (s,t) gamma2-def-manuell
set weight (ss,ts) lex2-def-manuell
set weight (s,ts) majo2-def-manuell

call operators-strategy { 1 } { [1] } delta2-def-manuell
call activate-lemma  delta2-def-manuell

call operators-strategy { 1 } { [1] } :ind-lemmas { alpha2-def-manuell beta2-def-manuell gamma2-def-manuell majo2-def-manuell lex2-def-manuell } lpo2-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { lpo2-def-manuell alpha2-def-manuell } alpha2-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { majo2-def-manuell beta2-def-manuell } beta2-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { majo2-def-manuell lex2-def-manuell gamma2-def-manuell } gamma2-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { lpo2-def-manuell majo2-def-manuell } majo2-def-manuell
call operators-strategy { 1 } { [1] } :ind-lemmas { lpo2-def-manuell lex2-def-manuell } lex2-def-manuell

call activate-lemmas { lpo2-def-manuell
		       alpha2-def-manuell
		       beta2-def-manuell
    		       gamma2-def-manuell
		       majo2-def-manuell
		       lex2-def-manuell }

assume
    { lpo2(s,t) = lpo1(s,t),
      Well(s) =/= true,
      Well(t) =/= true  }
    lpo2-lpo1
assume
    { alpha2(ss,s) = alpha1(ss,s),
      Well_tl(ss) =/= true,
      Well(s) =/= true  }
    alpha2-alpha1
assume
    { beta2(s,t) = beta1(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true   }
    beta2-beta1
assume
    { gamma2(s,t) = gamma1(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Fun(t) =/= true }
    gamma2-gamma1
assume
    { delta2(s,t) = delta1(s,t),
      Well(s) =/= true,
      Well(t) =/= true,
      Fun(s) =/= true,
      Var(t) =/= true   }
    delta2-delta1
assume
    { majo2(s,ts) = majo1(s,ts),
      Well(s) =/= true,
      Well_tl(ts) =/= true }
    majo2-majo1
assume
    { lex2(ss,ts) = lex1(ss,ts),
      length(ss) =/= length(ts),
      Well_tl(ss) =/= true, 
      Well_tl(ts) =/= true }
    lex2-lex1

set weight (s,t,0) lpo2-lpo1
set weight (ss,s) alpha2-alpha1
set weight (s,t) beta2-beta1
set weight (s,t) gamma2-gamma1
set weight (ss,ts) lex2-lex1
set weight (s,ts) majo2-majo1

call deactivate-lemmas  { lpo1-Lpo alpha1-Alpha beta1-Beta gamma1-Gamma delta1-Delta majo1-Majo lex1-Lex }

call operators-strategy  { 1 1 } { [1] [2] } delta2-delta1
call activate-lemma  delta2-delta1 :obl-litnbs-list { }

call deactivate-axioms  { Alpha-1 Alpha-2 Alpha-3 Alpha-4 Beta-1 Beta-2 Gamma-1 Gamma-2 Gamma-3 Delta-1 delta2-1 gamma2-1 gamma2-2 beta2-1 alpha2-1 alpha2-2 alpha2-3 }
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { alpha2-alpha1 beta2-beta1 gamma2-gamma1 } lpo2-lpo1
call activate-axioms  { alpha2-3 alpha2-2 alpha2-1 beta2-1 gamma2-2 gamma2-1 delta2-1 Delta-1 Gamma-3 Gamma-2 Gamma-1 Beta-2 Beta-1 Alpha-4 Alpha-3 Alpha-2 Alpha-1 }
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { alpha2-alpha1 lpo2-lpo1 } alpha2-alpha1
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { beta2-beta1 majo2-majo1 } beta2-beta1
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { majo2-majo1 lex2-lex1 gamma2-gamma1 } gamma2-gamma1
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { majo2-majo1 lpo2-lpo1 } majo2-majo1
call operators-strategy  { 1 1 } { [1] [2] } :ind-lemmas { lpo2-lpo1 lex2-lex1 } lex2-lex1

call activate-lemma  lpo1-Lpo :obl-litnbs-list { }
call activate-lemma  alpha1-Alpha :obl-litnbs-list { }
call activate-lemma  beta1-Beta :obl-litnbs-list { }
call activate-lemma  gamma1-Gamma :obl-litnbs-list { }
call activate-lemma  majo1-Majo :obl-litnbs-list { }
call activate-lemma  lex1-Lex :obl-litnbs-list { }

call activate-lemma  lpo2-lpo1 :obl-litnbs-list { }
call activate-lemma  alpha2-alpha1 :obl-litnbs-list { }
call activate-lemma  beta2-beta1 :obl-litnbs-list { }
call activate-lemma  gamma2-gamma1 :obl-litnbs-list { }
call activate-lemma  majo2-majo1 :obl-litnbs-list { }
call activate-lemma  lex2-lex1 :obl-litnbs-list { }

declare operators
    Lpoeq : Term Term --> Bool
    .

assert Lpoeq-1 :
    Lpoeq(s,t) = true
    if s = t
    .
assert Lpoeq-2 :
    Lpoeq(s,t) = Lpo(s,t)
    if s =/= t
    .

call analyze-operator  Lpoeq :speculate-domain-lemma-p FALSE
assume
    { def Lpoeq(s,t),
      Well(s) =/= true,
      Well(t) =/= true }
    Lpoeq-def-manuell
call operators-strategy  { 1 } { [1] } Lpoeq-def-manuell
call activate-lemma  Lpoeq-def-manuell

assume
    { Lpo(t1,t3) = true,
      subterm(t2,t1) =/= true,
      Lpoeq(t2,t3) =/= true,
      Well(t1) =/= true,
      Well(t2) =/= true,
      Well(t3) =/= true }
    Lemma2
call operators-strategy  { 1 2 3 } { [1] [1] [1] } Lemma2
call activate-lemma  Lemma2 :head-litnbs { 1 } :obl-litnbs-list { { 2 } { 3 } }

declare operators
    lexM2 : Term Termlist Termlist --> Bool
    .

assert lexM2-1 :
    lexM2(s,nil,nil) = false
    .
assert lexM2-2 :
    lexM2(u,cons(s,ss),cons(t,ts)) = lexM2(u,ss,ts)
    if s = t
    .
assert lexM2-3 :
    lexM2(u,cons(s,ss),cons(t,ts)) = and(lpo2(s,t),majo2(u,ts))
    if
      s =/= t
    .

call analyze-operator  lexM2 :speculate-domain-lemma-p FALSE
assume
    {  def lexM2(u,ss,ts),
      Well(u) =/= true,
      Well_tl(ss) =/= true,
      Well_tl(ts) =/= true,
      length(ss) =/= length(ts)}
    lexM2-def-manuell
call auto-strategy  lexM2-def-manuell
call activate-lemma  lexM2-def-manuell

assume
    { Lpo(F(f,ss1),t) = true,
      Lpo(s,t) =/= true,
      sublist(cons(s,ss),ss1) =/= true,
      Well(F(f,ss1)) =/= true,
      Well(t) =/= true,
      Well(s) =/= true,
      Well_tl(ss) =/= true }
    Lpo-sublist
call simplify  Lpo-sublist
call activate-lemma  Lpo-sublist

assume
    { lexM2(s,ss,ts) = and(lex2(ss,ts),majo2(s,ts)),
      sublist(ss,ss1) =/= true,
      Well(s) =/= true,
      Well_tl(ss) =/= true,
      Well_tl(ts) =/= true,
      length(ss) =/= length(ts),
      s =/= F(f,ss1) }
    lexM2-lex2-majo2
call auto-strategy  lexM2-lex2-majo2
call activate-lemma  lexM2-lex2-majo2