-- LOGPROOF


Derivation of

Any q:
(  perm([1,2,3],p)
 & append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any Q0:
  (  perm([2,3],Q0)
   & insert(1,Q0,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any Q0:
  (  Any Q1:
     (  perm([3],Q1)
      & insert(2,Q1,Q0))
   & insert(1,Q0,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any Q0:
  (  Any Q1:
     (  Any Q2:
        (  perm([],Q2)
         & insert(3,Q2,Q1))
      & insert(2,Q1,Q0))
   & insert(1,Q0,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any Q0:
  (  Any Q1:
     (  insert(3,[],Q1)
      & insert(2,Q1,Q0))
   & insert(1,Q0,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any Q0:
  (  insert(2,[3],Q0)
   & insert(1,Q0,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    insert(1,[2,3],p)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any q:
    (append(q,[2],[1,2,3]))
|   Any P4:
    (  insert(1,[3],P4)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L6:
    (append(L6,[2],[2,3]))
|   Any P4:
    (  insert(1,[3],P4)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L9:
    (append(L9,[2],[3]))
|   Any P4:
    (  insert(1,[3],P4)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,2,3]
  & Any L12:
    (append(L12,[2],[]))
|   Any P4:
    (  insert(1,[3],P4)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    Any P4:
    (  insert(1,[3],P4)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [2,1,3]
  & Any q:
    (append(q,[2],[2,1,3]))
|   Any P4:
    (  Any P5:
       (  insert(1,[],P5)
        & P4 = 3:P5)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [2,1,3]
  & Any L15:
    (append(L15,[2],[1,3]))
|   Any P4:
    (  Any P5:
       (  insert(1,[],P5)
        & P4 = 3:P5)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [2,1,3]
  & Any L18:
    (append(L18,[2],[3]))
|   Any P4:
    (  Any P5:
       (  insert(1,[],P5)
        & P4 = 3:P5)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [2,1,3]
  & Any L21:
    (append(L21,[2],[]))
|   Any P4:
    (  Any P5:
       (  insert(1,[],P5)
        & P4 = 3:P5)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    Any P4:
    (  Any P5:
       (  insert(1,[],P5)
        & P4 = 3:P5)
     & p = 2:P4)
  & Any q:
    (append(q,[2],p))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [2,3,1]
  & Any q:
    (append(q,[2],[2,3,1]))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [2,3,1]
  & Any L24:
    (append(L24,[2],[3,1]))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [2,3,1]
  & Any L27:
    (append(L27,[2],[1]))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [2,3,1]
  & Any L30:
    (append(L30,[2],[]))
|   Any Q0:
    (  Any P3:
       (  insert(2,[],P3)
        & Q0 = 3:P3)
     & insert(1,Q0,p))
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  Any Q0:
  (  Any P3:
     (  insert(2,[],P3)
      & Q0 = 3:P3)
   & insert(1,Q0,p))
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

  insert(1,[3,2],p)
& Any q:
  (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,3,2]
  & Any q:
    (append(q,[2],[1,3,2]))
|   Any P6:
    (  insert(1,[2],P6)
     & p = 3:P6)
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,3,2]
  & Any L33:
    (append(L33,[2],[3,2]))
|   Any P6:
    (  insert(1,[2],P6)
     & p = 3:P6)
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    p = [1,3,2]
  & Any L36:
    (append(L36,[2],[2]))
|   Any P6:
    (  insert(1,[2],P6)
     & p = 3:P6)
  & Any q:
    (append(q,[2],p))

Narrowing the preceding formula leads to the formula

    Any P6:
    (  insert(1,[2],P6)
     & p = 3:P6)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]

Narrowing the preceding formula leads to the formula

    p = [3,1,2]
  & Any q:
    (append(q,[2],[3,1,2]))
|   Any P6:
    (  Any P7:
       (  insert(1,[],P7)
        & P6 = 2:P7)
     & p = 3:P6)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]

Narrowing the preceding formula leads to the formula

    p = [3,1,2]
  & Any L42:
    (append(L42,[2],[1,2]))
|   Any P6:
    (  Any P7:
       (  insert(1,[],P7)
        & P6 = 2:P7)
     & p = 3:P6)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]

Narrowing the preceding formula leads to the formula

    p = [3,1,2]
  & Any L45:
    (append(L45,[2],[2]))
|   Any P6:
    (  Any P7:
       (  insert(1,[],P7)
        & P6 = 2:P7)
     & p = 3:P6)
  & Any q:
    (append(q,[2],p))
| p = [1,3,2]

Narrowing the preceding formula leads to the formula

  p = [1,3,2]
|   Any P6:
    (  Any P7:
       (  insert(1,[],P7)
        & P6 = 2:P7)
     & p = 3:P6)
  & Any q:
    (append(q,[2],p))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

  p = [1,3,2]
|   p = [3,2,1]
  & Any q:
    (append(q,[2],[3,2,1]))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

  p = [1,3,2]
|   p = [3,2,1]
  & Any L51:
    (append(L51,[2],[2,1]))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

  p = [1,3,2]
|   p = [3,2,1]
  & Any L54:
    (append(L54,[2],[1]))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

  p = [1,3,2]
|   p = [3,2,1]
  & Any L57:
    (append(L57,[2],[]))
| p = [3,1,2]

Narrowing the preceding formula leads to the formula

  p = [1,3,2]
| p = [3,1,2]

Number of proof steps: 35