reconsider TT = Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1))))) as InitHalting good Program of SCM+FSA by Lm10;
reconsider WT = while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))))) as InitHalting good Program of SCM+FSA by Lm4, Th11;
reconsider t14 = ((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),(intloc 0))) as InitHalting good Program of SCM+FSA ;
reconsider t16 = (t14 ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1)))) as good Program of SCM+FSA ;
( (t16 ";" WT) ";" TT is good & (t16 ";" WT) ";" TT is InitHalting ) ;
hence ((((((((intloc (1 + 1)) :=len (fsloc 0)) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" (((fsloc 0),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (4 + 1)))))) is InitHalting good Program of SCM+FSA ; :: thesis: verum