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:
set I1 = I ';' (Stop SCM+FSA);
set JI2 = ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA);
A1: ProgramPart (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) = ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) by RELAT_1:209;
A2: ProgramPart (if=0 (a,I,J)) = if=0 (a,I,J) by RELAT_1:209;
set s2 = s +* (Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)));
set P2 = P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA));
A3: ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) c= P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by FUNCT_4:26;
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 s5 = Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),2);
set i = a =0_goto ((card J) + 3);
A4: Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) c= s +* (Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))) by FUNCT_4:26;
IC in dom (Initialize (if=0 (a,I,J))) by COMPOS_1:141;
then A5: IC (s +* (Initialize (if=0 (a,I,J)))) = IC (Initialize (if=0 (a,I,J))) by FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A6: 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 A7: if=0 (a,I,J) c= s +* (Initialize (if=0 (a,I,J))) by A6, XBOOLE_1:1;
A8: if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:26;
A9: if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA)) by SCMFSA6A:67
.= ((a =0_goto ((card J) + 3)) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA))) by SCMFSA6A:67
.= (a =0_goto ((card J) + 3)) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))) by SCMFSA6A:71
.= (a =0_goto ((card J) + 3)) ';' ((J ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA))) by SCMFSA6A:67
.= (a =0_goto ((card J) + 3)) ';' (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by SCMFSA6A:67
.= (Macro (a =0_goto ((card J) + 3))) ';' (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by SCMFSA6A:def 6 ;
then Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),(card (Macro (a =0_goto ((card J) + 3))))) c= if=0 (a,I,J) by Lm1;
then A10: Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= if=0 (a,I,J) by COMPOS_1:150;
then Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= s +* (Initialize (if=0 (a,I,J))) by A7, XBOOLE_1:1;
then A11: Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),2) by AMI_1:81;
A12: Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= P +* (if=0 (a,I,J)) by A10, A8, XBOOLE_1:1;
A13: not a in dom (Initialize (if=0 (a,I,J))) by SCMFSA6B:12;
A14: 0 in dom (if=0 (a,I,J)) by Lm2;
A15: if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:26;
A16: (P +* (if=0 (a,I,J))) . 0 = (if=0 (a,I,J)) . 0 by A14, FUNCT_4:14
.= a =0_goto ((card J) + 3) by Lm3 ;
A17: 1 in dom (if=0 (a,I,J)) by Lm2;
A18: 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 A5, A16, PBOOLE:158 ;
assume s . a <> 0 ; :: thesis:
then (s +* (Initialize (if=0 (a,I,J)))) . a <> 0 by A13, FUNCT_4:12;
then A19: IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1)) = succ 0 by A5, A18, SCMFSA_2:96
.= 0 + 1 ;
A20: (P +* (if=0 (a,I,J))) . 1 = (if=0 (a,I,J)) . 1 by A17, A15, GRFUNC_1:8
.= goto 2 by Lm3 ;
assume A21: J is_closed_on s,P ; :: thesis:
A22: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),(1 + 1)) = Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1))) by A19, A20, PBOOLE:158 ;
A23: DataPart (s +* (Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))) = DataPart (s +* (Initialize (if=0 (a,I,J)))) by COMPOS_1:138, SCMFSA8A:14;

A24: now

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

end;

now

let a be Int-Location ; :: thesis:
thus (s +* (Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))) . a = (s +* (Initialize (if=0 (a,I,J)))) . a by A23, SCMFSA6A:38
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1)) . a by A18, SCMFSA_2:96
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),2)) . a by A22, SCMFSA_2:95 ; :: thesis:

end;

then A25: DataPart (s +* (Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))) = DataPart (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),2)) by A24, SCMFSA6A:38;
assume A26: J is_halting_on s,P ; :: thesis:
then A27: ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is_closed_on s,P by A21, SCMFSA8A:58;
then A28: ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is_closed_on s +* (Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by Th10;
A29: P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) halts_on s +* (Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))) by A21, A26, SCMFSA8A:59;
A30: IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),2)) = 2 by A22, SCMFSA_2:95;

now

let k be Element of NAT ; :: thesis:
( k = 0 or 0 + 1 < k + 1 ) by XREAL_1:8;
then A31: ( k = 0 or 1 <= k ) by NAT_1:13;

per cases by A31, XXREAL_0:1;

suppose A32: 1 < k ; :: thesis:

then consider k1 being Nat such that
A33: k1 + 1 = k by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
0 + 1 < k1 + 1 by A32, A33;
then consider k2 being Nat such that
A34: k2 + 1 = k1 by NAT_1:6;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 13;
reconsider m = IC (Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))),k2)) as Element of NAT ;
A35: card (if=0 (a,I,J)) = (card (Macro (a =0_goto ((card J) + 3)))) + (card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))) by A9, SCMFSA6A:61
.= 2 + (card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))) by COMPOS_1:150 ;
m in dom (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by A27, SCMFSA7B:def 7, A1;
then m < card (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by AFINSQ_1:70;
then A36: m + 2 < card (if=0 (a,I,J)) by A35, 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 A33, EXTPRO_1:5
.= IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),1)),1)),k2)) by A34, EXTPRO_1:5
.= IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J)))),(1 + 1))),k2)) by EXTPRO_1:5
.= m + 2 by A4, A28, A11, A30, A25, Th11, A12, A3 ;
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 A36, 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 A14, A5, EXTPRO_1:3; :: thesis:

end;

suppose k = 1 ; :: 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 A19, Lm2; :: thesis:

end;