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 Initialized s & J is_halting_on Initialized 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 Initialized s & J is_halting_on Initialized 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 Initialized s & J is_halting_on Initialized 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 COMPOS_1:150;
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 RELAT_1:209;
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 COMPOS_1:38;
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 EXTPRO_1:4
.= Following ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J))))) by EXTPRO_1:3
.= 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 Initialized s or not J is_halting_on Initialized 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 Initialized s ; :: thesis: ( not J is_halting_on Initialized 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 COMPOS_1:38;
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:123;
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 EXTPRO_1:4
.= 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 Initialized 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 Initialized 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:123;
x: Comput ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))),((LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))))) by EXTPRO_1:5;
A24: CurInstr ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(Comput ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))),((LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 2)))) = CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))),2))),(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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))))))) by x, T
.= IncAddr ((CurInstr ((ProgramPart (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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(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, EXTPRO_1:def 14
.= 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 EXTPRO_1:30;

now

let l be Element of NAT ; :: thesis: ( l < (LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 2 implies CurInstr ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(Comput ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))),b₁))) <> halt SCM+FSA )
assume A26: l < (LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 2 ; :: thesis: CurInstr ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(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 EXTPRO_1:3;
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 COMPOS_1:38;
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 COMPOS_1:38;
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:123;
TX3: 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)))),l)) by AMI_1:123;

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

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

then CurInstr ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(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 (s +* (Initialized (if>0 (a,I,J))))),(Comput ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))),l))) <> halt SCM+FSA by A8, A4, Y; :: thesis: verum

end;

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

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

end;

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

assume A28: CurInstr ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(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;
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 EXTPRO_1:5;
InsCode (CurInstr ((ProgramPart (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)))),l2)))) = InsCode (IncAddr ((CurInstr ((ProgramPart (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)))),l2)))),2)) by SCMFSA_4:22
.= InsCode (CurInstr ((ProgramPart (Comput ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))),2))),(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 (s +* (Initialized (if>0 (a,I,J))))),(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 (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)))),l2))) = halt SCM+FSA by SCMFSA_2:122;
n + 1 < ((LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 1) + 1 by A26, A29;
then n < (LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 1 by XREAL_1:8;
then l2 < LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))) by A30, XREAL_1:8;
hence contradiction by A22, A31, EXTPRO_1:def 14; :: thesis: verum

end;

end;

end;

then for l being Element of NAT st CurInstr ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(Comput ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))),l))) = halt SCM+FSA holds
(LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 2 <= l ;
then A32: LifeSpan ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J))))) = (LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 2 by A24, A25, EXTPRO_1:def 14;
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:123;
A33: DataPart (Result ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))))) by A22, EXTPRO_1:23
.= 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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 2))) by EXTPRO_1:5
.= DataPart (Result ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))))) by A25, A32, EXTPRO_1:23 ;

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 ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(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 ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))))) . x by A35, A37, A40, FUNCT_4:12, SCMFSA_2:84
.= (Result ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(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 ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))))) . x by A35, A37, A42, FUNCT_4:12, SCMFSA_2:85
.= (Result ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(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:123;
A46: IC (Result ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(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, COMPOS_1:3, FUNCT_4:12
.= ((card I) + (card J)) + 1 by A15, A21, SCMFSA8A:61 ;
thus (IExec ((if>0 (a,I,J)),s)) . x = (Result ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))))) . x by A35, A37, A44, COMPOS_1:3, FUNCT_4:12
.= (Comput ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))),((LifeSpan ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))) + 2))) . x by A25, A32, EXTPRO_1:23
.= 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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)))))))) by A44, EXTPRO_1:5
.= (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 ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))))))) + 2 by A1, A23, A12, A17, A20, Th11, T
.= (IC (Result ((ProgramPart (s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))),(s +* (Initialized (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))))))) + 2 by A22, EXTPRO_1:23
.= (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 COMPOS_1:3;
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 FUNCT_4:122 ;
:: thesis: verum