thus Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) is good ; :: thesis: Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) is InitHalting
let s be State of SCM+FSA; :: according to SCM_HALT:def 2 :: thesis: ( not Initialize K592((intloc 0),1) c= s or for b₁ being set holds
( not Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) c= b₁ or b₁ halts_on s ) )
assume Z1: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for b₁ being set holds
( not Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) c= P or P halts_on s )
assume Z2: Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) c= P ; :: thesis: P halts_on s
ZZ2: P +* (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))) = P by Z2, FUNCT_4:104;
A1: not ((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))) destroys intloc (1 + 1) by Lm22;
X2: dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:19;
intloc 0 <> IC by SCMFSA_2:81;
then X1: dom ((intloc 0) .--> 1) misses {(IC )} by X2, ZFMISC_1:17;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
then Start-At (0,SCM+FSA) c= s by Z1, XBOOLE_1:1;
then x: s = Initialize s by FUNCT_4:104;
Y2: intloc 0 in dom ((intloc 0) .--> 1) by X2, TARSKI:def 1;
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
then dom ((intloc 0) .--> 1) misses dom (Start-At (0,SCM+FSA)) by X1;
then (intloc 0) .--> 1 c= Initialize ((intloc 0) .--> 1) by FUNCT_4:33;
then (intloc 0) .--> 1 c= s by Z1, XBOOLE_1:1;
then A2: s . (intloc 0) = ((intloc 0) .--> 1) . (intloc 0) by Y2, GRFUNC_1:8
.= 1 by FUNCOP_1:87 ;
Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) is_halting_on s,P by A1, A2, SCM_HALT:75;
then P +* (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom ((intloc (2 + 1)),(intloc 0)))) ';' ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ';' ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ';' (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ';' (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ';' (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))) halts_on Initialize s by SCMFSA7B:def 8;
hence P halts_on s by x, ZZ2; :: thesis: verum