let s be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_on s & I is_halting_on s holds
( if=0 (a,I,J) is_closed_on s & if=0 (a,I,J) is_halting_on s )
let I, J be Program of SCM+FSA; :: thesis: for a being read-write Int-Location st s . a = 0 & I is_closed_on s & I is_halting_on s holds
( if=0 (a,I,J) is_closed_on s & if=0 (a,I,J) is_halting_on s )
let a be read-write Int-Location ; :: thesis: ( s . a = 0 & I is_closed_on s & I is_halting_on s implies ( if=0 (a,I,J) is_closed_on s & if=0 (a,I,J) is_halting_on s ) )
set I1 = I ';' (Stop SCM+FSA);
set s1 = s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)));
set s3 = s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)));
set s4 = Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1);
set i = a =0_goto ((card J) + 3);
A1: not a in dom ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by SCMFSA6B:12;
A2: 0 in dom (if=0 (a,I,J)) by Lm2;
if=0 (a,I,J) c= (if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then dom (if=0 (a,I,J)) c= dom ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
then A3: (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . 0 = ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) . 0 by A2, FUNCT_4:14
.= (if=0 (a,I,J)) . 0 by A2, SCMFSA6B:7
.= a =0_goto ((card J) + 3) by Lm3 ;
IC SCM+FSA in dom ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
then A4: IC (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) = IC ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A5: if=0 (a,I,J) c= (if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
(if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)) c= s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then A6: if=0 (a,I,J) c= s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by A5, XBOOLE_1:1;
A7: if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA)) by SCMFSA6A:67;
card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) = card (((Macro (a =0_goto ((card J) + 3))) ';' J) ';' (Goto ((card I) + 1))) by SCMFSA6A:def 6
.= (card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1))) by SCMFSA6A:61
.= (card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + 1 by SCMFSA8A:29
.= ((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1 by SCMFSA6A:61
.= ((card J) + 2) + 1 by COMPOS_1:150
.= (card J) + (2 + 1) ;
then ProgramPart (Relocated ((I ';' (Stop SCM+FSA)),((card J) + 3))) c= if=0 (a,I,J) by A7, Lm1;
then ProgramPart (Relocated ((I ';' (Stop SCM+FSA)),((card J) + 3))) c= s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by A6, XBOOLE_1:1;
then ProgramPart (ProgramPart (Relocated ((I ';' (Stop SCM+FSA)),((card J) + 3)))) c= Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1) by AMI_1:99;
then A8: ProgramPart (Relocated ((I ';' (Stop SCM+FSA)),((card J) + 3))) c= Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1) by RELAT_1:209;
Y: (ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) /. (IC (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) = (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . (IC (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by COMPOS_1:38;
A9: Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),(0 + 1)) = Following ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),0))) by EXTPRO_1:4
.= Following ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by EXTPRO_1:3
.= Exec ((a =0_goto ((card J) + 3)),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by A4, A3, Y ;
A10: DataPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) = DataPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) by SCMFSA6A:39, SCMFSA8A:14;

A11: now

let f be FinSeq-Location ; :: thesis: (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . f = (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) . f
thus (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . f = (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . f by A10, SCMFSA6A:38
.= (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) . f by A9, SCMFSA_2:96 ; :: thesis: verum

end;

now

let a be Int-Location ; :: thesis: (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . a = (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) . a
thus (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) . a = (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . a by A10, SCMFSA6A:38
.= (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) . a by A9, SCMFSA_2:96 ; :: thesis: verum

end;

then A12: DataPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) = DataPart (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) by A11, SCMFSA6A:38;
assume s . a = 0 ; :: thesis: ( not I is_closed_on s or not I is_halting_on s or ( if=0 (a,I,J) is_closed_on s & if=0 (a,I,J) is_halting_on s ) )
then (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . a = 0 by A1, FUNCT_4:12;
then A13: IC (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) = (card J) + 3 by A9, SCMFSA_2:96;
assume A14: I is_closed_on s ; :: thesis: ( not I is_halting_on s or ( if=0 (a,I,J) is_closed_on s & if=0 (a,I,J) is_halting_on s ) )
assume A15: I is_halting_on s ; :: thesis: ( if=0 (a,I,J) is_closed_on s & if=0 (a,I,J) is_halting_on s )
then A16: I ';' (Stop SCM+FSA) is_closed_on s by A14, SCMFSA8A:46;
I ';' (Stop SCM+FSA) is_halting_on s by A14, A15, SCMFSA8A:46;
then A17: ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
DataPart s = DataPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11;
then A18: I ';' (Stop SCM+FSA) is_closed_on s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by A16, Th6;
A19: (I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)) c= s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;

now

let k be Element of NAT ; :: thesis: IC (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),b₁)) in dom (if=0 (a,I,J))

per cases ( 0 < k or k = 0 ) ;

suppose 0 < k ; :: thesis: IC (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),b₁)) in dom (if=0 (a,I,J))

then consider k1 being Nat such that
A20: k1 + 1 = k by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider m = IC (Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),k1)) as Element of NAT ;
m in dom (I ';' (Stop SCM+FSA)) by A16, SCMFSA7B:def 7;
then A21: m < card (I ';' (Stop SCM+FSA)) by AFINSQ_1:70;
card (Stop SCM+FSA) = 1 by COMPOS_1:46;
then A22: card (I ';' (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:61;
card (if=0 (a,I,J)) = ((card I) + (card J)) + 4 by Th14
.= ((card J) + 3) + (card (I ';' (Stop SCM+FSA))) by A22 ;
then A23: m + ((card J) + 3) < card (if=0 (a,I,J)) by A21, XREAL_1:8;
T: ProgramPart (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) = ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) by AMI_1:123;
IC (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k)) = IC (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)),k1)) by A20, EXTPRO_1:5
.= m + ((card J) + 3) by A19, A18, A8, A13, A12, Th11, T ;
hence IC (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k)) in dom (if=0 (a,I,J)) by A23, AFINSQ_1:70; :: thesis: verum

end;

suppose k = 0 ; :: thesis: IC (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),b₁)) in dom (if=0 (a,I,J))

hence IC (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k)) in dom (if=0 (a,I,J)) by A2, A4, EXTPRO_1:3; :: thesis: verum

end;

end;

end;

hence if=0 (a,I,J) is_closed_on s by SCMFSA7B:def 7; :: thesis: if=0 (a,I,J) is_halting_on s
T: ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) by AMI_1:123;
x: Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) + 1)) = Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)),(LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))))) by EXTPRO_1:5;
CurInstr ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) + 1)))) = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1))),(Comput ((ProgramPart (Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1))),(Comput ((ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)),(LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))))))) by x, T
.= IncAddr ((CurInstr ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))))))),((card J) + 3)) by A19, A18, A8, A13, A12, Th11
.= IncAddr ((halt SCM+FSA),((card J) + 3)) by A17, EXTPRO_1:def 14
.= halt SCM+FSA by SCMFSA_4:8 ;
then ProgramPart (s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((if=0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by EXTPRO_1:30;
hence if=0 (a,I,J) is_halting_on s by SCMFSA7B:def 8; :: thesis: verum