------------------------------------------      ---------------------------------------- 
                                        {s+1+c-1=a+b,c<>0} s:=s+1 {s+c-1=a+b,c<>0}      {s+c-1=a+b,c<>0}   c:=c-1 {s+c=a+b,c<>0}        
                                       ---------------------------------------------------------------------------------------------
(s+c=a+b ∧ c<>0) -> (s+1+c-1=a+b ∧ c<>0)                            {s+1+c-1=a+b, c<>0} s:=s+1; c:=c-1 {s+c=a+b, c<>0}
------------------------------------------------------------------------------------------------------------------------
                                 {s+c=a+b,c<>0} s:=s+1; c:=c-1 {s+c=a+b,c<>0}                                             (s+c=a+b ∧ c<>0) -> s+c=a+b
                               ----------------------------------------------------------------------------------------------------------------------
                                                                                {s+c=a+b,c<>0} s:=s+1; c:=c-1 {s+c=a+b}