-- LISTREVPROOF


Derivation of

    reverse(s) = s'
==>   s ~ s'
    & (    sorted(s)
       ==> sortedB(s'))

Applying fixpoint induction w.r.t.

  reverse[] = []
& (     reverse(x:s) = z0++[x]
   <=== reverse(s) = z0)

to the preceding tree leads to the formula

All x s2 z0:
(  reverse0([],[])
 & (     reverse0(x:s2,z0++[x])
    <=== reverse0(s2,z0)))

Applying the axiom

     reverse0(s,s')
===>   s ~ s'
     & (    sorted(s)
        ==> sortedB(s'))

at positions [0,1,1],[0,1,0],[0,0] of the preceding tree leads to the formula

All x s2 z0:
(  (  [] ~ []
    & (    sorted[]
       ==> sortedB[]))
 & (       x:s2 ~ z0++[x]
         & (    sorted(x:s2)
            ==> sortedB(z0++[x]))
    <===   s2 ~ z0
         & (    sorted(s2)
            ==> sortedB(z0))))

Simplifying (9 steps) the preceding tree leads to new ones. The current factor is given by

    sorted[]
==> sortedB[]

Narrowing the preceding factor leads to the factor

sortedB[]

Narrowing the preceding factor leads to new ones. The current factor is given by

All x s2 z0:
(      s2 ~ z0
     & (    sorted(s2)
        ==> sortedB(z0))
 ==> x:s2 ~ z0++[x])

Applying the theorem

     x:s ~ s'++[x]
<=== s ~ s'

at position [1] of the preceding factor leads to the factor

All x1 s2 z0:
(      s2 ~ z0
     & (    sorted(s2)
        ==> sortedB(z0))
 ==> s2 ~ z0)

Simplifying (3 steps) the preceding factor leads to a new formula. The current formula is given by

All x s2 z0:
(      s2 ~ z0
     & (    sorted(s2)
        ==> sortedB(z0))
     & sorted(x:s2)
 ==> sortedB(z0++[x]))

Applying the theorem

     sortedB(s'++[x])
<===   s ~ s'
     & (    sorted(s)
        ==> sortedB(s'))
     & sorted(x:s)

at position [0,1] of the preceding tree leads to the formula

All x2 s2 z0:
(      s2 ~ z0
     & (    sorted(s2)
        ==> sortedB(z0))
     & sorted(x2:s2)
 ==> Any s3:
     (  s3 ~ z0
      & (    sorted(s3)
         ==> sortedB(z0))
      & sorted(x2:s3)))

Simplifying (2 steps) the preceding tree leads to the formula

True

The following solutions were computed:

True