-- NEEDproof


Derivation of

f(f(x,y),z) = 0

Narrowing the preceding formula leads to 

f(f(x,y),0) = 0 & z = 0 | Any y0:(2 = 0 & z = suc(y0))

Narrowing the preceding formula leads to 

(f(0,0) = 0 & x = 0 & y = 0 | Any x1:(f(1,0) = 0 & x = suc(x1) & y = 0) | 
 Any y1:(f(2,0) = 0 & y = suc(y1))) & 
z = 0 | 
Any y0:(2 = 0 & z = suc(y0))

Narrowing the preceding formula leads to 

(0 = 0 & x = 0 & y = 0 | Any x1:(f(1,0) = 0 & x = suc(x1) & y = 0) | 
 Any y1:(f(2,0) = 0 & y = suc(y1))) & 
z = 0 | 
Any y0:(2 = 0 & z = suc(y0))

Narrowing the preceding formula leads to 

(0 = 0 & x = 0 & y = 0 | Any x1:(1 = 0 & x = suc(x1) & y = 0) | 
 Any y1:(f(2,0) = 0 & y = suc(y1))) & 
z = 0 | 
Any y0:(2 = 0 & z = suc(y0))

Narrowing the preceding formula leads to 

(0 = 0 & x = 0 & y = 0 | Any x1:(1 = 0 & x = suc(x1) & y = 0) | 
 Any y1:(1 = 0 & y = suc(y1))) & 
z = 0 | 
Any y0:(2 = 0 & z = suc(y0))

Simplifying the preceding formula (21 steps) leads to 

x = 0 & y = 0 & z = 0

Number of proof steps: 6

Solutions:

x = 0 & y = 0 & z = 0