let I, J be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location
for s being State of SCM+FSA st s . a <= 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )
let a be read-write Int-Location ; :: thesis: for s being State of SCM+FSA st s . a <= 0 & J is_closed_on Initialize s & J is_halting_on Initialize s holds
IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )
let s be State of SCM+FSA ; :: thesis: ( s . a <= 0 & J is_closed_on Initialize s & J is_halting_on Initialize s implies IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) )
set I1 = I ';' (Stop SCM+FSA );
set JI2 = ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA );
set s2 = s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )));
set s3 = s +* (Initialized (if>0 a,I,J));
set s4 = Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1;
set s5 = Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2;
set i = a >0_goto ((card J) + 3);
A1: (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))) by FUNCT_4:26, SCMFSA6B:8;
if>0 a,I,J c= Initialized (if>0 a,I,J) by SCMFSA6A:26;
then A2: dom (if>0 a,I,J) c= dom (Initialized (if>0 a,I,J)) by GRFUNC_1:8;
A3: 0 in dom (if>0 a,I,J) by Lm2;
then A4: (s +* (Initialized (if>0 a,I,J))) . 0 = (Initialized (if>0 a,I,J)) . 0 by A2, FUNCT_4:14
.= (if>0 a,I,J) . 0 by A3, SCMFSA6A:50
.= a >0_goto ((card J) + 3) by Lm3 ;
A5: if>0 a,I,J c= Initialized (if>0 a,I,J) by SCMFSA6A:26;
A6: 1 in dom (if>0 a,I,J) by Lm2;
A7: (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1) . 1 = (s +* (Initialized (if>0 a,I,J))) . 1 by AMI_1:54
.= (Initialized (if>0 a,I,J)) . 1 by A2, A6, FUNCT_4:14
.= (if>0 a,I,J) . 1 by A6, SCMFSA6A:50
.= goto 2 by Lm3 ;
IC SCM+FSA in dom (Initialized (if>0 a,I,J)) by SCMFSA6A:24;
then A8: IC (s +* (Initialized (if>0 a,I,J))) = (Initialized (if>0 a,I,J)) . (IC SCM+FSA ) by FUNCT_4:14
.= 0 by SCMFSA6A:46 ;
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 ProgramPart (Relocated (((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 A9: ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),2) c= if>0 a,I,J by SCMFSA7B:6;
A10: not a in dom (Initialized (if>0 a,I,J)) by SCMFSA6A:48;
A11: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) /\ NAT by SCMFSA6A:34
.= NAT by XBOOLE_1:21 ;
Initialized (if>0 a,I,J) c= s +* (Initialized (if>0 a,I,J)) by FUNCT_4:26;
then if>0 a,I,J c= s +* (Initialized (if>0 a,I,J)) by A5, XBOOLE_1:1;
then ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),2) c= s +* (Initialized (if>0 a,I,J)) by A9, XBOOLE_1:1;
then ProgramPart (ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),2)) c= Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2 by AMI_1:99;
then A12: ProgramPart (Relocated (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),2) c= Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2 by AMI_1:105;
Y: (ProgramPart (s +* (Initialized (if>0 a,I,J)))) /. (IC (s +* (Initialized (if>0 a,I,J)))) = (s +* (Initialized (if>0 a,I,J))) . (IC (s +* (Initialized (if>0 a,I,J)))) by AMI_1:150;
A13: Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),(0 + 1) = Following (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),0 ) by AMI_1:14
.= Following (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))) by AMI_1:13
.= Exec (a >0_goto ((card J) + 3)),(s +* (Initialized (if>0 a,I,J))) by A8, A4, Y ;
assume s . a <= 0 ; :: thesis: ( not J is_closed_on Initialize s or not J is_halting_on Initialize s or IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) )
then (s +* (Initialized (if>0 a,I,J))) . a <= 0 by A10, FUNCT_4:12;
then A14: IC (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1) = succ 0 by A8, A13, SCMFSA_2:97
.= 0 + 1 ;
assume A15: J is_closed_on Initialize s ; :: thesis: ( not J is_halting_on Initialize s or IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) )
Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1)) /. (IC (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1)) = (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1) . (IC (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1)) by AMI_1:150;
T: ProgramPart (s +* (Initialized (if>0 a,I,J))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1) by AMI_1:144;
A16: Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),(1 + 1) = Following (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1) by AMI_1:14
.= Exec (goto 2),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1) by A14, A7, Y, T ;
then A17: IC (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) = 2 by SCMFSA_2:95;
A18: DataPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))) = DataPart (s +* (Initialized (if>0 a,I,J))) by SCMFSA6A:39, SCMFSA6A:53;

A19: now

let f be FinSeq-Location ; :: thesis: (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))) . f = (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) . f
thus (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))) . f = (s +* (Initialized (if>0 a,I,J))) . f by A18, SCMFSA6A:38
.= (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1) . f by A13, SCMFSA_2:97
.= (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) . f by A16, SCMFSA_2:95 ; :: thesis: verum

end;

now

let a be Int-Location ; :: thesis: (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))) . a = (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) . a
thus (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))) . a = (s +* (Initialized (if>0 a,I,J))) . a by A18, SCMFSA6A:38
.= (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),1) . a by A13, SCMFSA_2:97
.= (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) . a by A16, SCMFSA_2:95 ; :: thesis: verum

end;

then A20: DataPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))) = DataPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) by A19, SCMFSA6A:38;
assume A21: J is_halting_on Initialize s ; :: thesis: IExec (if>0 a,I,J),s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )
then A22: ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))) by A15, SCMFSA8A:60;
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ) is_closed_on Initialize s by A15, A21, SCMFSA8A:58;
then A23: ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))) by Th9;
T: ProgramPart (s +* (Initialized (if>0 a,I,J))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) by AMI_1:144;
x: Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),((LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2) = Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) by AMI_1:51;
A24: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),((LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2))),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),((LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2)) = CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))))),(Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))))) by x, T
.= IncAddr (CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))))),(Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))))),2 by A1, A23, A12, A17, A20, Th11
.= IncAddr (halt SCM+FSA ),2 by A22, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
then A25: ProgramPart (s +* (Initialized (if>0 a,I,J))) halts_on s +* (Initialized (if>0 a,I,J)) by AMI_1:146;

now

let l be Element of NAT ; :: thesis: ( l < (LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2 implies CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁) <> halt SCM+FSA )
assume A26: l < (LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2 ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁) <> halt SCM+FSA
u: Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),0 = s +* (Initialized (if>0 a,I,J)) by AMI_1:13;
Y: (ProgramPart (s +* (Initialized (if>0 a,I,J)))) /. (IC (s +* (Initialized (if>0 a,I,J)))) = (s +* (Initialized (if>0 a,I,J))) . (IC (s +* (Initialized (if>0 a,I,J)))) by AMI_1:150;
Z: (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l)) /. (IC (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l)) = (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l) . (IC (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l)) by AMI_1:150;

per cases ( l = 0 or l = 1 or ( l <> 0 & l <> 1 ) ) ;

suppose l = 0 ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁) <> halt SCM+FSA

then CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l) = CurInstr (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))) by u;
hence CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l) <> halt SCM+FSA by A8, A4, Y, SCMFSA_2:49, SCMFSA_2:124; :: thesis: verum

end;

suppose l = 1 ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁) <> halt SCM+FSA

hence CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l) <> halt SCM+FSA by A14, A7, Z, SCMFSA_2:47, SCMFSA_2:124; :: thesis: verum

end;

suppose A27: ( l <> 0 & l <> 1 ) ; :: thesis: not CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),b₁) = halt SCM+FSA

assume A28: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l) = halt SCM+FSA ; :: thesis: contradiction
consider n being Nat such that
A29: l = n + 1 by A27, NAT_1:6;
n <> 0 by A27, A29;
then consider l2 being Nat such that
A30: n = l2 + 1 by NAT_1:6;
reconsider l2 = l2 as Element of NAT by ORDINAL1:def 13;
T: ProgramPart (s +* (Initialized (if>0 a,I,J))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),(1 + 1)) by AMI_1:144;
x: Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),(l2 + (1 + 1)) = Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),(1 + 1)),l2 by AMI_1:51;
InsCode (CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),l2)),(Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),l2)) = InsCode (IncAddr (CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),l2)),(Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),l2)),2) by SCMFSA_4:22
.= InsCode (CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2),l2)),(Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2),l2)) by A1, A23, A12, A17, A20, Th11
.= InsCode (CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),(l2 + (1 + 1)))),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),(l2 + (1 + 1)))) by x, T
.= 0 by A29, A30, A28, SCMFSA_2:124 ;
then A31: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),l2)),(Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),l2) = halt SCM+FSA by SCMFSA_2:122;
n + 1 < ((LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 1) + 1 by A26, A29;
then n < (LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 1 by XREAL_1:8;
then l2 < LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))) by A30, XREAL_1:8;
hence contradiction by A22, A31, AMI_1:def 46; :: thesis: verum

end;

end;

end;

then for l being Element of NAT st CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l)),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),l) = halt SCM+FSA holds
(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2 <= l ;
then A32: LifeSpan (s +* (Initialized (if>0 a,I,J))) = (LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2 by A24, A25, AMI_1:def 46;
T: ProgramPart (s +* (Initialized (if>0 a,I,J))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) by AMI_1:144;
A33: DataPart (Result (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))))) by A22, AMI_1:122
.= DataPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))))) by A1, A23, A12, A17, A20, Th11, T
.= DataPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),((LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2)) by AMI_1:51
.= DataPart (Result (s +* (Initialized (if>0 a,I,J)))) by A25, A32, AMI_1:122 ;

A34: now

let x be set ; :: thesis: ( x in dom (IExec (if>0 a,I,J),s) implies (IExec (if>0 a,I,J),s) . b₁ = ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . b₁ )
A35: ( x in dom (s | NAT ) implies x is Element of NAT ) by RELAT_1:86;
A36: dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) = {(IC SCM+FSA )} by FUNCOP_1:19;
A37: IExec (if>0 a,I,J),s = (Result (s +* (Initialized (if>0 a,I,J)))) +* (s | NAT ) by SCMFSA6B:def 1;
A38: IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s = (Result (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) +* (s | NAT ) by SCMFSA6B:def 1;
assume A39: x in dom (IExec (if>0 a,I,J),s) ; :: thesis: (IExec (if>0 a,I,J),s) . b₁ = ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . b₁

per cases ( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Element of NAT ) by A39, SCMFSA6A:35;

suppose A40: x is Int-Location ; :: thesis: (IExec (if>0 a,I,J),s) . b₁ = ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . b₁

then x <> IC SCM+FSA by SCMFSA_2:81;
then A41: not x in dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A36, TARSKI:def 1;
thus (IExec (if>0 a,I,J),s) . x = (Result (s +* (Initialized (if>0 a,I,J)))) . x by A35, A37, A40, FUNCT_4:12, SCMFSA_2:84
.= (Result (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) . x by A33, A40, SCMFSA6A:38
.= (IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) . x by A35, A38, A40, FUNCT_4:12, SCMFSA_2:84
.= ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . x by A41, FUNCT_4:12 ; :: thesis: verum

end;

suppose A42: x is FinSeq-Location ; :: thesis: (IExec (if>0 a,I,J),s) . b₁ = ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . b₁

then x <> IC SCM+FSA by SCMFSA_2:82;
then A43: not x in dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A36, TARSKI:def 1;
thus (IExec (if>0 a,I,J),s) . x = (Result (s +* (Initialized (if>0 a,I,J)))) . x by A35, A37, A42, FUNCT_4:12, SCMFSA_2:85
.= (Result (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) . x by A33, A42, SCMFSA6A:38
.= (IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) . x by A35, A38, A42, FUNCT_4:12, SCMFSA_2:85
.= ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . x by A43, FUNCT_4:12 ; :: thesis: verum

end;

suppose A44: x = IC SCM+FSA ; :: thesis: (IExec (if>0 a,I,J),s) . b₁ = ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . b₁

then A45: x in dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A36, TARSKI:def 1;
T: ProgramPart (s +* (Initialized (if>0 a,I,J))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2) by AMI_1:144;
A46: IC (Result (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) = IC (IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) by A35, A38, A44, AMI_1:48, FUNCT_4:12
.= ((card I) + (card J)) + 1 by A15, A21, SCMFSA8A:61 ;
thus (IExec (if>0 a,I,J),s) . x = (Result (s +* (Initialized (if>0 a,I,J)))) . x by A35, A37, A44, AMI_1:48, FUNCT_4:12
.= (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),((LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))) + 2)) . x by A25, A32, AMI_1:122
.= IC (Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(Comput (ProgramPart (s +* (Initialized (if>0 a,I,J)))),(s +* (Initialized (if>0 a,I,J))),2),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))))) by A44, AMI_1:51
.= (IC (Comput (ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ))))))) + 2 by A1, A23, A12, A17, A20, Th11, T
.= (IC (Result (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )))))) + 2 by A22, AMI_1:122
.= (Start-At ((((card I) + (card J)) + 1) + 2),SCM+FSA ) . (IC SCM+FSA ) by A46, FUNCOP_1:87
.= ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . x by A44, A45, FUNCT_4:14 ; :: thesis: verum

end;

suppose A47: x is Element of NAT ; :: thesis: (IExec (if>0 a,I,J),s) . b₁ = ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . b₁

then x <> IC SCM+FSA by AMI_1:48;
then A48: not x in dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A36, TARSKI:def 1;
A49: x in NAT by A47;
hence (IExec (if>0 a,I,J),s) . x = (s | NAT ) . x by A11, A37, FUNCT_4:14
.= (IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) . x by A11, A38, A49, FUNCT_4:14
.= ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . x by A48, FUNCT_4:12 ;
:: thesis: verum

end;

end;

end;

dom (IExec (if>0 a,I,J),s) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom ((IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) by PARTFUN1:def 4 ;
hence IExec (if>0 a,I,J),s = (IExec (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A34, FUNCT_1:9
.= ((IExec J,s) +* (Start-At (((card I) + (card J)) + 1),SCM+FSA )) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A15, A21, SCMFSA8A:62
.= (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by AMI_1:141 ;
:: thesis: verum