set D = Int-Locations \/ FinSeq-Locations ;
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 J0 = Directed J;
set s0 = Initialize s;
set J9 = J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )));
set s00 = s +* ((Directed J) +* (Start-At (insloc 0 )));
set s3 = s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )));
set s4 = Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1;
set s5 = Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2;
set i = a =0_goto (insloc ((card J) + 3));
assume s . a <> 0 ; :: thesis:
then A1: (Initialize s) . a <> 0 by SCMFSA6C:3;
A2: (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a = s . a by Th28
.= (Initialize s) . a by SCMFSA6C:3 ;
assume A3: Directed J is_pseudo-closed_on s ; :: thesis:
A4: if=0 a,I,J = ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1;
A5: (Directed J) +* (Start-At (insloc 0 )) c= s +* ((Directed J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
DataPart s = DataPart (s +* ((Directed J) +* (Start-At (insloc 0 )))) by SCMFSA8A:11;
then A6: Directed J is_pseudo-closed_on s +* ((Directed J) +* (Start-At (insloc 0 ))) by A3, Th52;
A7: insloc 0 in dom (if=0 a,I,J) by Th54;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A8: dom (if=0 a,I,J) c= dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
IC SCM+FSA in dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
then A9: IC (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = ((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
A10: (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A7, A8, FUNCT_4:14
.= (if=0 a,I,J) . (insloc 0 ) by A7, SCMFSA6B:7
.= a =0_goto (insloc ((card J) + 3)) by Th55 ;
then A11: CurInstr (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = a =0_goto (insloc ((card J) + 3)) by A9;

A12: now

thus Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(0 + 1) = Following (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 ) by AMI_1:14
.= Following (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by AMI_1:13
.= Exec (a =0_goto (insloc ((card J) + 3))),(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by A9, A10 ; :: thesis:

end;

A13: now

thus IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) = Next (IC (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))) by A1, A2, A12, SCMFSA_2:96
.= insloc (0 + 1) by A9 ; :: thesis:

end;

A14: insloc 1 in dom (if=0 a,I,J) by Th54;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A15: dom (if=0 a,I,J) c= dom ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;

A16: now

thus (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . (insloc 1) = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 1) by AMI_1:54
.= ((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 1) by A14, A15, FUNCT_4:14
.= (if=0 a,I,J) . (insloc 1) by A14, SCMFSA6B:7
.= goto (insloc 2) by Th55 ; :: thesis:

end;

A17: Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(1 + 1) = Following (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) by AMI_1:14
.= Exec (goto (insloc 2)),(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) by A13, A16 ;
A18: card (Macro (a =0_goto (insloc ((card J) + 3)))) = 2 by SCMFSA7B:6;
A19: (if=0 a,I,J) +* (Start-At (insloc 0 )) c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A20: if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by A19, XBOOLE_1:1;
if=0 a,I,J = (((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA )) by A4, SCMFSA6A:67;
then if=0 a,I,J = ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA ))) by SCMFSA6A:67;
then if=0 a,I,J = (Macro (a =0_goto (insloc ((card J) + 3)))) ';' (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))) by SCMFSA6A:67;
then ProgramPart (Relocated (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))),2) c= if=0 a,I,J by A18, FUNCT_4:26;
then ProgramPart (Relocated (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))),2) c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by A20, XBOOLE_1:1;
then ProgramPart [(ProgramPart (Relocated (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))),2))] c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2 by AMI_1:99;
then A21: ProgramPart (Relocated (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))),2) c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2 by AMI_1:105;
ProgramPart (Relocated (Directed J),2) c= ProgramPart (Relocated (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))),2) by Th12, SCMFSA6A:55;
then A22: ProgramPart (Relocated (Directed J),2) c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2 by A21, XBOOLE_1:1;
A23: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) = insloc 2 by A17, SCMFSA_2:95;
A24: DataPart (s +* ((Directed J) +* (Start-At (insloc 0 )))) = DataPart (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) by SCMFSA6A:39, SCMFSA8A:14;

A25: now

let a be Int-Location ; :: thesis:
thus (s +* ((Directed J) +* (Start-At (insloc 0 )))) . a = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a by A24, SCMFSA6A:38
.= (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . a by A12, SCMFSA_2:96
.= (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) . a by A17, SCMFSA_2:95 ; :: thesis:

end;

now

let f be FinSeq-Location ; :: thesis:
thus (s +* ((Directed J) +* (Start-At (insloc 0 )))) . f = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . f by A24, SCMFSA6A:38
.= (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . f by A12, SCMFSA_2:96
.= (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) . f by A17, SCMFSA_2:95 ; :: thesis:

end;

then A26: DataPart (s +* ((Directed J) +* (Start-At (insloc 0 )))) = DataPart (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) by A25, SCMFSA6A:38;
A27: if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26, SCMFSA6B:5;

now

thus card (if=0 a,I,J) = ((card I) + (card J)) + (2 + 2) by SCMFSA8B:14
.= ((card J) + 2) + ((card I) + 2) ; :: thesis:

end;

then A28: ((card J) + 2) + 0 < card (if=0 a,I,J) by XREAL_1:10;
then A29: insloc ((card J) + 2) in dom (if=0 a,I,J) by SCMFSA6A:15;
set ss = Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2);

A30: now

thus IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2)) = IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2),(pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J))) by AMI_1:51
.= (IC (Computation (s +* ((Directed J) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)))) + 2 by A5, A6, A22, A23, A26, Th51
.= (IC (Computation (s +* ((Directed J) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Directed J)))) + 2 by A3, Th50
.= (insloc (card (ProgramPart (Directed J)))) + 2 by A3, SCMFSA8A:def 5
.= (insloc (card (Directed J))) + 2 by AMI_1:105
.= insloc ((card J) + 2) by SCMFSA8A:34 ; :: thesis:

end;

then A31: CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2)) = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc ((card J) + 2)) by AMI_1:54
.= (if=0 a,I,J) . (insloc ((card J) + 2)) by A27, A29, GRFUNC_1:8
.= goto (insloc (((card I) + (card J)) + 3)) by Th63 ;
A32: if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26, SCMFSA6B:5;

now

thus card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ; :: thesis:

end;

then ((card I) + (card J)) + 3 < card (if=0 a,I,J) by NAT_1:13;
then A33: insloc (((card I) + (card J)) + 3) in dom (if=0 a,I,J) by SCMFSA6A:15;

A34: now

thus IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(((pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2) + 1)) = IC (Following (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2))) by AMI_1:14
.= insloc (((card I) + (card J)) + 3) by A31, SCMFSA_2:95 ; :: thesis:

end;

then A35: CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(((pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2) + 1)) = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc (((card I) + (card J)) + 3)) by AMI_1:54
.= (if=0 a,I,J) . (insloc (((card I) + (card J)) + 3)) by A32, A33, GRFUNC_1:8
.= halt SCM+FSA by Th61 ;
then A36: s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
hence if=0 a,I,J is_halting_on s by SCMFSA7B:def 8; :: thesis:

now

let k be Element of NAT ; :: thesis:

per cases ;

suppose k = 0 ; :: thesis:

then Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k = s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))) by AMI_1:13;
then IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = insloc 0 by Th31;
hence IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by Th54; :: thesis:

end;

suppose ( 0 < k & k = 1 ) ; :: thesis:

hence IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by A13, Th54; :: thesis:

end;

suppose A37: ( 0 < k & k <> 1 & k < (pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2 ) ; :: thesis:

then 0 + 1 <= k by INT_1:20;
then 1 < k by A37, XXREAL_0:1;
then 0 + (1 + 1) <= k by INT_1:20;
then consider k2 being Nat such that
A38: 2 + k2 = k by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 13;
A39: k2 < pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J) by A37, A38, XREAL_1:8;
then A40: k2 < pseudo-LifeSpan s,(Directed J) by A3, Th50;
A41: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2),k2) by A38, AMI_1:51
.= (IC (Computation (s +* ((Directed J) +* (Start-At (insloc 0 )))),k2)) + 2 by A5, A6, A22, A23, A26, A39, Th51 ;
reconsider n = IC (Computation (s +* ((Directed J) +* (Start-At (insloc 0 )))),k2) as Element of NAT by ORDINAL1:def 13;
insloc n in dom (Directed J) by A3, A40, SCMFSA8A:31;
then n < card (Directed J) by SCMFSA6A:15;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:8;
then A43: n + 2 < (card J) + 2 by SCMFSA8A:34;
card (if=0 a,I,J) = ((card I) + (card J)) + (2 + 2) by SCMFSA8B:14
.= ((card J) + 2) + ((card I) + 2) ;
then (card J) + 2 <= card (if=0 a,I,J) by NAT_1:12;
then n + 2 < card (if=0 a,I,J) by A43, XXREAL_0:2;
hence IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by A41, SCMFSA6A:15; :: thesis:

end;

suppose A44: ( 0 < k & k <> 1 & (pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2 <= k ) ; :: thesis:

hereby :: thesis:

per cases ) + 2 = k or (pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2 < k ) by A44, XXREAL_0:1;

suppose (pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2 = k ; :: thesis:

hence IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by A28, A30, SCMFSA6A:15; :: thesis:

end;

suppose (pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2 < k ; :: thesis:

then ((pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 2) + 1 <= k by INT_1:20;
hence IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J) by A33, A34, A35, AMI_1:52; :: thesis:

end;

hence if=0 a,I,J is_closed_on s by SCMFSA7B:def 7; :: thesis:

now

let k be Element of NAT ; :: thesis:
assume A45: CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA ; :: thesis:
assume A46: not (pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + (1 + 2) <= k ; :: thesis:
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 ) = a =0_goto (insloc ((card J) + 3)) by A11, AMI_1:13;
then A47: ( k <> 0 & k <> 1 ) by A13, A16, A45, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:124;
0 + 2 < ((card I) + (card J)) + 3 by XREAL_1:10;
then A48: ( insloc 2 in dom (if=0 a,I,J) & (if=0 a,I,J) . (insloc 2) <> halt SCM+FSA ) by Th56;
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2) = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 2) by A23, AMI_1:54
.= (if=0 a,I,J) . (insloc 2) by A48, Th26 ;
then 2 < k by A45, A47, A48, NAT_1:27;
then consider k2 being Nat such that
A49: 2 + k2 = k by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 13;
k < ((pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 1) + 2 by A46;
then k2 < (pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 1 by A49, XREAL_1:8;
then A50: k2 <= pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J) by NAT_1:13;
reconsider n = IC (Computation (s +* ((Directed J) +* (Start-At (insloc 0 )))),k2) as Element of NAT by ORDINAL1:def 13;
A52: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),2),k2) by A49, AMI_1:51
.= insloc (n + 2) by A5, A6, A22, A23, A26, A50, Th51 ;
A53: k2 <= pseudo-LifeSpan s,(Directed J) by A3, A50, Th50;

A54: now

per cases by A53, XXREAL_0:1;

suppose k2 = pseudo-LifeSpan s,(Directed J) ; :: thesis:

then IC (Computation (s +* ((Directed J) +* (Start-At (insloc 0 )))),k2) = insloc (card (ProgramPart (Directed J))) by A3, SCMFSA8A:def 5
.= insloc (card (Directed J)) by AMI_1:105 ;
then A55: n = card J by SCMFSA8A:34;
((card I) + (card J)) + (2 + 1) = (((card J) + 2) + 1) + (card I) ;
then ((card J) + 2) + 1 <= ((card I) + (card J)) + 3 by NAT_1:11;
hence n + 2 < ((card I) + (card J)) + 3 by A55, NAT_1:13; :: thesis:

end;

suppose k2 < pseudo-LifeSpan s,(Directed J) ; :: thesis:

then insloc n in dom (Directed J) by A3, SCMFSA8A:31;
then n < card (Directed J) by SCMFSA6A:15;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:8;
then A56: n + 2 < (card J) + 2 by SCMFSA8A:34;
((card I) + (card J)) + (1 + 2) = ((card J) + 2) + ((card I) + 1) ;
then (card J) + 2 <= ((card I) + (card J)) + 3 by NAT_1:11;
hence n + 2 < ((card I) + (card J)) + 3 by A56, XXREAL_0:2; :: thesis:

end;

then A57: ( insloc (n + 2) in dom (if=0 a,I,J) & (if=0 a,I,J) . (insloc (n + 2)) <> halt SCM+FSA ) by Th56;
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) by AMI_1:54
.= (if=0 a,I,J) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) by A52, A57, Th26 ;
hence contradiction by A45, A52, A54, Th56; :: thesis:

end;

then A58: LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (pseudo-LifeSpan (s +* ((Directed J) +* (Start-At (insloc 0 )))),(Directed J)) + 3 by A35, A36, AMI_1:def 46;
pseudo-LifeSpan s,(Directed J) = LifeSpan (s +* ((J ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) by A3, Th58;
hence LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((J ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 3 by A3, A58, Th50; :: thesis: