-- PERMPROOF


Derivation of

    sort(s) = s'
==> s ~ s'

Applying fixpoint induction w.r.t.

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

to the preceding tree leads to the formula

All x y s7 z3 z4 s1 s2:
(  sort1([],[])
 & sort1([x],[x])
 & (     sort1(x:(y:s7),merge(z3,z4))
    <===   split(s7) = (s1,s2)
         & sort1(x:s1,z3)
         & sort1(y:s2,z4)))

Applying the axiom

     sort1(s,s')
===> s ~ s'

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

All x y s7 z3 z4 s1 s2:
(  [] ~ []
 & [x] ~ [x]
 & (     x:(y:s7) ~ merge(z3,z4)
    <===   split(s7) = (s1,s2)
         & x:s1 ~ z3
         & y:s2 ~ z4))

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

All x y s7 s1 s2:
(    split(s7) = (s1,s2)
 ==> x:(y:s7) ~ merge(x:s1,y:s2))

Applying the theorem

     split(s) = (s1,s2)
===> s ~ s1++s2

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

All x y s7 s8 s9:
(    s7 ~ s8++s9
 ==> x:(y:s7) ~ merge(x:s8,y:s9))

Applying the theorem

     s ~ merge(s1,s2)
<=== s ~ s1++s2

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

All x y s7 s8 s9:
(    s7 ~ s8++s9
 ==> x:(y:s7) ~ (x:s8)++(y:s9))

Simplifying the preceding tree leads to the formula

All x y s7 s8 s9:
(    s7 ~ s8++s9
 ==> x:(y:s7) ~ x:(s8++(y:s9)))

Applying the theorem

x:y:(s1++s2) ~ x:(s1++(y:s2))

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

All x3 y2 s7 s8 s9:
(    s7 ~ s8++s9
 ==> True)

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

True

The following solutions were computed:

True