thus 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 good ; :: thesis: 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
let s be State of SCM+FSA; :: according to SCM_HALT:def 2 :: thesis: ( not Initialize K560((intloc 0),1) c= s or for b₁ being set holds
( not 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))))) c= b₁ or b₁ halts_on s ) )
assume Z1: Initialize ((intloc 0) .--> 1) c= s ; :: thesis: for b₁ being set holds
( not 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))))) c= b₁ or b₁ halts_on s )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not 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))))) c= P or P halts_on s )
assume Z2: 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))))) c= P ; :: thesis: P halts_on s
B: P +* (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)))))) = P by Z2, FUNCT_4:98;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:25;
then Start-At (0,SCM+FSA) c= s by Z1, XBOOLE_1:1;
then C: Initialize s = s by FUNCT_4:98;
A: not ((((((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))) destroys intloc (3 + 1) by Lm6;
dom ((intloc 0) .--> 1) = {(intloc 0)} by FUNCOP_1:13;
then D: intloc 0 in dom ((intloc 0) .--> 1) by TARSKI:def 1;
F: IC <> intloc 0 by SCMFSA_2:56;
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then E: not intloc 0 in dom (Start-At (0,SCM+FSA)) by F, TARSKI:def 1;
dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1;
then intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by D, XBOOLE_0:def 3;
then s . (intloc 0) = (Initialize ((intloc 0) .--> 1)) . (intloc 0) by Z1, GRFUNC_1:2
.= ((intloc 0) .--> 1) . (intloc 0) by E, FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
then 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_halting_on s,P by A, SCM_HALT:62;
then P +* (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)))))) halts_on Initialize s by SCMFSA7B:def 7;
hence P halts_on s by B, C; :: thesis: verum