thus Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) is good ; :: thesis: Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) is InitHalting
let s be State of SCM+FSA; :: according to SCM_HALT:def 1 :: thesis: ( not Initialize K546((),1) c= s or for b1 being set holds
( not Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) c= b1 or b1 halts_on s ) )

assume A1: Initialize (() .--> 1) c= s ; :: thesis: for b1 being set holds
( not Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) c= b1 or b1 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 (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) c= P or P halts_on s )
assume A2: Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) c= P ; :: thesis: P halts_on s
A3: P +* (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))) = P by ;
Start-At (0,SCM+FSA) c= Initialize (() .--> 1) by FUNCT_4:25;
then Start-At (0,SCM+FSA) c= s by ;
then A4: Initialize s = s by FUNCT_4:98;
A5: not ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))) destroys intloc (3 + 1) by Lm6;
A6: intloc 0 in dom (() .--> 1) by TARSKI:def 1;
A7: IC <> intloc 0 by SCMFSA_2:56;
A8: not intloc 0 in dom () by ;
dom (Initialize (() .--> 1)) = (dom (() .--> 1)) \/ (dom ()) by FUNCT_4:def 1;
then intloc 0 in dom (Initialize (() .--> 1)) by ;
then s . () = (Initialize (() .--> 1)) . () by
.= (() .--> 1) . () by
.= 1 by FUNCOP_1:72 ;
then Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) is_halting_on s,P by ;
then P +* (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))) halts_on Initialize s by SCMFSA7B:def 7;
hence P halts_on s by A3, A4; :: thesis: verum