-- PARTN2proof


Derivation of

partn(s,n) = p ==> lgOk(n,p)

Hoare invariant creation for the iterative program

partn(s,n) = g(n,s,0,[],[])

at position [] of the preceding formula leads to 

INV(s,n,s,0,[],[]) & 
(g(n,z3,z4,z5,z6) = p & INV(s,n,z3,z4,z5,z6) ==> lgOk(n,p))

Narrowing at position [0] of the preceding formula (2 steps) leads to 

True & (g(n,z3,z4,z5,z6) = p & INV(s,n,z3,z4,z5,z6) ==> lgOk(n,p))

Reducts have been simplified.

Simplifying the preceding formula leads to 

g(n,z3,z4,z5,z6) = p & INV(s,n,z3,z4,z5,z6) ==> lgOk(n,p)

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

g(n,z3,z4,z5,z6) = p ==> (INV(s,n,z3,z4,z5,z6) ==> lgOk(n,p))

Applying fixpoint induction w.r.t.

g(n,[],k,s,p) = p++[s] & 
(g(n,x:s,k,s',p) = z7 <=== k < n & g(n,s,k+1,s'++[x],p) = z7) & 
(g(n,x:s,k,s',p) = z7 <=== k > n & g(n,x:s,0,[],p++[s']) = z7)

at position [] of the preceding formula leads to 

All n k s p s4:(INV(s4,n,[],k,s,p) ==> lgOk(n,p++[s])) & 
All n k s p x s' z7 s5:(k < n & 
                        All s5:(INV(s5,n,s,k+1,s'++[x],p) ==> lgOk(n,z7)) & 
                        INV(s5,n,x:s,k,s',p) ==> 
                        lgOk(n,z7)) & 
All n k s p x s' z7 s6:(k > n & 
                        All s6:(INV(s6,n,x:s,0,[],p++[s']) ==> lgOk(n,z7)) & 
                        INV(s6,n,x:s,k,s',p) ==> 
                        lgOk(n,z7))

Reducts have been simplified.

Applying the axiom resp. theorem

INV(s,n,s1,k,s2,p) <=== lgOk(n,p) & k = length(s2) & k <= n

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

All n s p:(length(s) <= n & lgOk(n,p) ==> lgOk(n,p++[s])) & 
All n p s' z7:(length(s') <= n & length(s') < n & 
               (lgOk(n,p) & length(s')+1 <= n ==> lgOk(n,z7)) & lgOk(n,p) ==> 
               lgOk(n,z7))

Reducts have been simplified.

Applying the axiom resp. theorem

lgOk(n,p++[s]) <=== lgOk(n,p) & length(s) <= n

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

All n p s' z7:(length(s') <= n & length(s') < n & 
               (lgOk(n,p) & length(s')+1 <= n ==> lgOk(n,z7)) & lgOk(n,p) ==> 
               lgOk(n,z7))

Applying the theorem

k < n ===> k+1 <= n

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

True

Reducts have been simplified.

Number of proof steps: 8

Solutions:

True