-- SORTPROOF


Derivation of

    sort(s) = s'
==> sorted(s')

Applying fixpoint induction w.r.t.

  sort[] = []
& sort[x] = [x]
& (     sort(x:(y:s)) = merge(z0,z1)
   <===   split(s) = (s1,s2)
        & sort(x:s1) = z0
        & sort(y:s2) = z1)

to the preceding tree leads to the formula

All x y s7 z0 z1 s1 s2:
(  sort0([],[])
 & sort0([x],[x])
 & (     sort0(x:(y:s7),merge(z0,z1))
    <===   split(s7) = (s1,s2)
         & sort0(x:s1,z0)
         & sort0(y:s2,z1)))

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

sort0([],[])

Narrowing the preceding factor leads to the factor

sorted[]

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

All x:
(sort0([x],[x]))

Narrowing the preceding factor leads to the factor

All x2:
(sorted[x2])

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

All x y s7 z0 z1 s1 s2:
(      split(s7) = (s1,s2)
     & sort0(x:s1,z0)
     & sort0(y:s2,z1)
 ==> sort0(x:(y:s7),merge(z0,z1)))

Applying the axiom

     sort0(s,s')
===> sorted(s')

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

All x y s7 z0 z1 s1 s2:
(      split(s7) = (s1,s2)
     & sorted(z0)
     & sorted(z1)
 ==> sorted(merge(z0,z1)))

Applying the theorem

       sorted(s)
     & sorted(s')
===> sorted(merge(s,s'))

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

All x y s7 z0 z1 s1 s2:
(      sorted(merge(z0,z1))
     & split(s7) = (s1,s2)
 ==> sorted(merge(z0,z1)))

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

True

The following solutions were computed:

True