The loop and Times Macroinstruction for SCMFSA
Noriko Asamoto · 2007
Let s be a state of SCMFSA and let P be an initial finite partial state of SCMFSA. We say that P is pseudo-closed on s if and only if the condition (Def. 1) is satisfied. (Def. 1) There exists a natural number k such that IC(Computation(s+·(P+·Start-At(insloc(0)))))(k) = insloc(cardProgramPart(P )) and for every natural number n such that n < k holds IC(Computation(s+·(P+·Start-At(insloc(0)))))(n) ∈ domP. Let P be an initial finite partial state of SCMFSA. We say that P is pseudoparaclosed if and only if: (Def. 2) For every state s of SCMFSA holds P is pseudo-closed on s.