Proof of Correctness: Recursion inside loop

Question

I am trying to prove the correctness of the algorithm in the research paper. It is at page 17 in the pdf.

    http://tinman.cs.gsu.edu/~raj/8710/f08/paraconsistent.pdf

The algorithm in short words, It finds models for the logic program by using relational approach.. The algorithm take each and every rule and builds the part of the model after performing algebraic approach.

Each rules runs certain number of times until stability is maintained which means LHS and RHS values are same. (Recursion) -- This recursion is inside the loop

I am trying to prove correctness of the algorithm. I am doing this out of my interest.

Terminating condition: Since there are 'n' rules in the program where n is finite, the algorithm terminates as the algorithm process for each and every rule.

Induction: Loop Invariant: Model= {R$_K$, Facts} where K= {1,2,3...m} m

Base : 
                  m=0  K=0  Model= {Facts}   

Hypothesis: 
               m=z,  K= {1,2...m}     Model= {R$_K$, Facts}

Inductive Step:                
                 m=z+1 K= {1,2,3...m} 

                     I have to prove recursion now. Got lost.       

Do I need to use strong induction for this? Help is appreciated.