-- LOGproof2


Derivation of

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

Narrowing the preceding formula leads to 

Any q:(Any q0:(perm([2,3],q0) & insert(1,q0,p)) & q++[2] = p)

Simplifying the preceding formula (2 steps) leads to 

Any q0:(perm([2,3],q0) & insert(1,q0,p)) & Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

Any q0:(Any q1:(perm([3],q1) & insert(2,q1,q0)) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

Any q0:(Any q1:(Any q2:(perm([],q2) & insert(3,q2,q1)) & insert(2,q1,q0)) & 
        insert(1,q0,p)) & 
Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

Any q0:(Any q1:(Any q2:(q2 = [] & insert(3,q2,q1)) & insert(2,q1,q0)) & 
        insert(1,q0,p)) & 
Any q:(q++[2] = p)

Simplifying the preceding formula (2 steps) leads to 

Any q0:(Any q1:(insert(3,[],q1) & insert(2,q1,q0)) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

Any q0:(Any q1:(q1 = 3:[] & insert(2,q1,q0)) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Simplifying the preceding formula (3 steps) leads to 

Any q0:(insert(2,[3],q0) & insert(1,q0,p)) & Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

Any q0:((q0 = 2:[3] | Any p5:(insert(2,[],p5) & q0 = 3:p5)) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Simplifying the preceding formula (6 steps) leads to 

insert(1,[2,3],p) & Any q:(q++[2] = p) | 
Any q0:(Any p5:(insert(2,[],p5) & q0 = 3:p5) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

(p = 1:[2,3] | Any p6:(insert(1,[3],p6) & p = 2:p6)) & Any q:(q++[2] = p) | 
Any q0:(Any p5:(insert(2,[],p5) & q0 = 3:p5) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Simplifying the preceding formula (9 steps) leads to 

Any p6:(insert(1,[3],p6) & p = 2:p6) & Any q:(q++[2] = p) | 
Any q0:(Any p5:(insert(2,[],p5) & q0 = 3:p5) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

Any p6:((p6 = 1:[3] | Any p7:(insert(1,[],p7) & p6 = 3:p7)) & p = 2:p6) & 
Any q:(q++[2] = p) | 
Any q0:(Any p5:(insert(2,[],p5) & q0 = 3:p5) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Simplifying the preceding formula (14 steps) leads to 

Any p6:(Any p7:(insert(1,[],p7) & p6 = 3:p7) & p = 2:p6) & Any q:(q++[2] = p) | 
Any q0:(Any p5:(insert(2,[],p5) & q0 = 3:p5) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

Any p6:(Any p7:(p7 = 1:[] & p6 = 3:p7) & p = 2:p6) & Any q:(q++[2] = p) | 
Any q0:(Any p5:(insert(2,[],p5) & q0 = 3:p5) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Simplifying the preceding formula (17 steps) leads to 

Any q0:(Any p5:(insert(2,[],p5) & q0 = 3:p5) & insert(1,q0,p)) & 
Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

Any q0:(Any p5:(p5 = 2:[] & q0 = 3:p5) & insert(1,q0,p)) & Any q:(q++[2] = p)

Simplifying the preceding formula (9 steps) leads to 

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

Narrowing the preceding formula leads to 

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

Simplifying the preceding formula (7 steps) leads to 

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

Narrowing the preceding formula leads to 

p = [1,3,2] | 
Any p10:((p10 = 1:[2] | Any p11:(insert(1,[],p11) & p10 = 2:p11)) & p = 3:p10) & 
Any q:(q++[2] = p)

Simplifying the preceding formula (13 steps) leads to 

p = [1,3,2] | p = [3,1,2] | 
Any p10:(Any p11:(insert(1,[],p11) & p10 = 2:p11) & p = 3:p10) & 
Any q:(q++[2] = p)

Narrowing the preceding formula leads to 

p = [1,3,2] | p = [3,1,2] | 
Any p10:(Any p11:(p11 = 1:[] & p10 = 2:p11) & p = 3:p10) & Any q:(q++[2] = p)

Simplifying the preceding formula (17 steps) leads to 

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

Number of proof steps: 24