let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let s be State of SCM+FSA; :: thesis:
let I, J be Program of SCM+FSA; :: thesis:
let a be read-write Int-Location ; :: thesis:
A1: ProgramPart (if=0 (a,I,J)) = if=0 (a,I,J) by RELAT_1:209;
set I1 = I ';' (Stop SCM+FSA);
A2: ProgramPart (I ';' (Stop SCM+FSA)) = I ';' (Stop SCM+FSA) by RELAT_1:209;
set s1 = s +* (Initialize (I ';' (Stop SCM+FSA)));
set P1 = P +* (I ';' (Stop SCM+FSA));
set s3 = s +* (Initialize (if=0 (a,I,J)));
set P3 = P +* (if=0 (a,I,J));
set s4 = Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1);
set i = a =0_goto ((card J) + 3);
A3: not a in dom (Initialize (if=0 (a,I,J))) by SCMFSA6B:12;
A4: 0 in dom (if=0 (a,I,J)) by Lm2;
A5: (P +* (if=0 (a,I,J))) . 0 = (if=0 (a,I,J)) . 0 by A4, FUNCT_4:14
.= a =0_goto ((card J) + 3) by Lm3 ;
IC in dom (Initialize (if=0 (a,I,J))) by COMPOS_1:141;
then A6: IC (s +* (Initialize (if=0 (a,I,J)))) = IC (Initialize (if=0 (a,I,J))) by FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A7: if=0 (a,I,J) c= Initialize (if=0 (a,I,J)) by SCMFSA8A:9;
Initialize (if=0 (a,I,J)) c= s +* (Initialize (if=0 (a,I,J))) by FUNCT_4:26;
then A8: if=0 (a,I,J) c= s +* (Initialize (if=0 (a,I,J))) by A7, XBOOLE_1:1;
A9: if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:26;
A10: 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 A11: Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= if=0 (a,I,J) by A10, Lm1;
then Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= s +* (Initialize (if=0 (a,I,J))) by A8, XBOOLE_1:1;
then A12: Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1) by AMI_1:81;
A13: Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= P +* (if=0 (a,I,J)) by A11, A9, XBOOLE_1:1;
A14: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),(0 + 1)) = Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),0))) by EXTPRO_1:4
.= Following ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J))))) by EXTPRO_1:3
.= Exec ((a =0_goto ((card J) + 3)),(s +* (Initialize (if=0 (a,I,J))))) by A6, A5, PBOOLE:158 ;
A15: DataPart (s +* (Initialize (I ';' (Stop SCM+FSA)))) = DataPart (s +* (Initialize (if=0 (a,I,J)))) by COMPOS_1:138, SCMFSA8A:14;

A16: now

let f be FinSeq-Location ; :: thesis:
thus (s +* (Initialize (I ';' (Stop SCM+FSA)))) . f = (s +* (Initialize (if=0 (a,I,J)))) . f by A15, SCMFSA6A:38
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1)) . f by A14, SCMFSA_2:96 ; :: thesis:

end;

now

let a be Int-Location ; :: thesis:
thus (s +* (Initialize (I ';' (Stop SCM+FSA)))) . a = (s +* (Initialize (if=0 (a,I,J)))) . a by A15, SCMFSA6A:38
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1)) . a by A14, SCMFSA_2:96 ; :: thesis:

end;

then A17: DataPart (s +* (Initialize (I ';' (Stop SCM+FSA)))) = DataPart (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1)) by A16, SCMFSA6A:38;
assume s . a = 0 ; :: thesis:
then (s +* (Initialize (if=0 (a,I,J)))) . a = 0 by A3, FUNCT_4:12;
then A18: IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1)) = (card J) + 3 by A14, SCMFSA_2:96;
assume A19: I is_closed_on s,P ; :: thesis:
assume A20: I is_halting_on s,P ; :: thesis:
then A21: I ';' (Stop SCM+FSA) is_closed_on s,P by A19, SCMFSA8A:46;
I ';' (Stop SCM+FSA) is_halting_on s,P by A19, A20, SCMFSA8A:46;
then A22: P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) by SCMFSA7B:def 8, A2;
DataPart s = DataPart (s +* (Initialize (I ';' (Stop SCM+FSA)))) by SCMFSA8A:11;
then A23: I ';' (Stop SCM+FSA) is_closed_on s +* (Initialize (I ';' (Stop SCM+FSA))),P +* (I ';' (Stop SCM+FSA)) by A21, Th6;
A24: Initialize (I ';' (Stop SCM+FSA)) c= s +* (Initialize (I ';' (Stop SCM+FSA))) by FUNCT_4:26;
A25: I ';' (Stop SCM+FSA) c= P +* (I ';' (Stop SCM+FSA)) by FUNCT_4:26;

now

let k be Element of NAT ; :: thesis:

per cases ;

suppose 0 < k ; :: thesis:

then consider k1 being Nat such that
A26: k1 + 1 = k by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider m = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k1)) as Element of NAT ;
m in dom (I ';' (Stop SCM+FSA)) by A21, SCMFSA7B:def 7, A2;
then A27: m < card (I ';' (Stop SCM+FSA)) by AFINSQ_1:70;
card (Stop SCM+FSA) = 1 by COMPOS_1:46;
then A28: 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 A28 ;
then A29: m + ((card J) + 3) < card (if=0 (a,I,J)) by A27, XREAL_1:8;
IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),k)) = IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1)),k1)) by A26, EXTPRO_1:5
.= m + ((card J) + 3) by A24, A23, A12, A18, A17, Th11, A25, A13 ;
hence IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),k)) in dom (if=0 (a,I,J)) by A29, AFINSQ_1:70; :: thesis:

end;

suppose k = 0 ; :: thesis:

hence IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),k)) in dom (if=0 (a,I,J)) by A4, A6, EXTPRO_1:3; :: thesis:

end;