let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I, J being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st s . a <> 0 & J is_closed_on Initialized s,P & J is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
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,P & J is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,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,P & J is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,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,P & J is_halting_on Initialized s,P implies IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,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 +* (Initialize ((intloc 0) .--> 1));
set P2 = P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA));
A1: ((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 ((intloc 0) .--> 1));
set P3 = P +* (if=0 (a,I,J));
set s4 = Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1);
set s5 = Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2);
set i = a =0_goto ((card J) + 3);
B2: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1) by FUNCT_4:26;
then A2: Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1)) by B2, XBOOLE_1:1;
0 in dom (if=0 (a,I,J)) by Lm2;
then A3: (P +* (if=0 (a,I,J))) . 0 = (if=0 (a,I,J)) . 0 by FUNCT_4:14
.= a =0_goto ((card J) + 3) by Lm3 ;
A5: 1 in dom (if=0 (a,I,J)) by Lm2;
A6: (P +* (if=0 (a,I,J))) . 1 = (if=0 (a,I,J)) . 1 by A5, FUNCT_4:14
.= goto 2 by Lm3 ;
V: Initialize ((intloc 0) .--> 1) c= Initialized (if=0 (a,I,J)) by FUNCT_4:26;
then dom (Initialize ((intloc 0) .--> 1)) c= dom (Initialized (if=0 (a,I,J))) by RELAT_1:25;
then B9: not a in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:48;
X2: IC in dom (Initialize ((intloc 0) .--> 1)) by COMPOS_1:225;
then A7: IC (s +* (Initialize ((intloc 0) .--> 1))) = IC (Initialize ((intloc 0) .--> 1)) by FUNCT_4:14
.= IC (Initialized (if=0 (a,I,J))) by V, X2, GRFUNC_1:8
.= 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
.= (Macro (a =0_goto ((card J) + 3))) ';' (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by SCMFSA6A:67 ;
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 A8: Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= if=0 (a,I,J) by COMPOS_1:150;
A10: dom (ProgramPart s) = NAT by COMPOS_1:34;
if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:26;
then A12: Reloc ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),2) c= P +* (if=0 (a,I,J)) by A8, XBOOLE_1:1;
A13: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),(0 + 1)) = Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),0))) by EXTPRO_1:4
.= Following ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1)))) by EXTPRO_1:3
.= Exec ((a =0_goto ((card J) + 3)),(s +* (Initialize ((intloc 0) .--> 1)))) by A7, A3, PBOOLE:158 ;
assume s . a <> 0 ; :: thesis: ( not J is_closed_on Initialized s,P or not J is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
then (s +* (Initialize ((intloc 0) .--> 1))) . a <> 0 by B9, FUNCT_4:12;
then A14: IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)) = succ 0 by A7, A13, SCMFSA_2:96
.= 0 + 1 ;
assume A15: J is_closed_on Initialized s,P ; :: thesis: ( not J is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
A16: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + 1)) = Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1))) by A14, A6, PBOOLE:158 ;
then A17: IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)) = 2 by SCMFSA_2:95;

A19: now

let f be FinSeq-Location ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . f = (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)) . f
thus (s +* (Initialize ((intloc 0) .--> 1))) . f = (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)) . f by A13, SCMFSA_2:96
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)) . f by A16, SCMFSA_2:95 ; :: thesis: verum

end;

now

let a be Int-Location ; :: thesis: (s +* (Initialize ((intloc 0) .--> 1))) . a = (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)) . a
thus (s +* (Initialize ((intloc 0) .--> 1))) . a = (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),1)) . a by A13, SCMFSA_2:96
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)) . a by A16, SCMFSA_2:95 ; :: thesis: verum

end;

then A20: DataPart (s +* (Initialize ((intloc 0) .--> 1))) = DataPart (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)) by A19, SCMFSA6A:38;
assume A21: J is_halting_on Initialized s,P ; :: thesis: IExec ((if=0 (a,I,J)),P,s) = (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
then A22: P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by A15, SCMFSA8A:60;
((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is_closed_on Initialized s,P by A15, A21, SCMFSA8A:58;
then A23: ((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is_closed_on s +* (Initialize ((intloc 0) .--> 1)),P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)) by Th9;
A24: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 2)))) = CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))))))) by EXTPRO_1:5
.= IncAddr ((CurInstr ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))))))),2) by A2, A23, A12, A17, A20, Th11, A1
.= IncAddr ((halt SCM+FSA),2) by A22, EXTPRO_1:def 14
.= halt SCM+FSA by COMPOS_1:93 ;
then A25: P +* (if=0 (a,I,J)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:30;

now

let l be Element of NAT ; :: thesis: ( l < (LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 implies CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b₁))) <> halt SCM+FSA )
assume A26: l < (LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 ; :: thesis: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b₁))) <> halt SCM+FSA
A27: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),0) = s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:3;

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

suppose l = 0 ; :: thesis: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b₁))) <> halt SCM+FSA

hence CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),l))) <> halt SCM+FSA by A7, A3, A27, PBOOLE:158; :: thesis: verum

end;

suppose l = 1 ; :: thesis: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b₁))) <> halt SCM+FSA

hence CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),l))) <> halt SCM+FSA by A14, A6, PBOOLE:158; :: thesis: verum

end;

suppose A28: ( l <> 0 & l <> 1 ) ; :: thesis: not CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),b₁))) = halt SCM+FSA

assume A29: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),l))) = halt SCM+FSA ; :: thesis: contradiction
consider n being Nat such that
A30: l = n + 1 by A28, NAT_1:6;
n <> 0 by A28, A30;
then consider l2 being Nat such that
A31: n = l2 + 1 by NAT_1:6;
reconsider l2 = l2 as Element of NAT by ORDINAL1:def 13;
A32: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),(l2 + (1 + 1))) = Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),(1 + 1))),l2) by EXTPRO_1:5;
InsCode (CurInstr ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),l2)))) = InsCode (IncAddr ((CurInstr ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),l2)))),2)) by COMPOS_1:def 38
.= 0 by A30, A31, A29, A32, A2, A23, A17, A20, Th11, A12, A1, SCMFSA_2:124 ;
then A33: CurInstr ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),l2))) = halt SCM+FSA by SCMFSA_2:122;
n + 1 < ((LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + 1 by A26, A30;
then n < (LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 by XREAL_1:8;
then l2 < LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) by A31, XREAL_1:8;
hence contradiction by A22, A33, EXTPRO_1:def 14; :: thesis: verum

end;

end;

end;

then for l being Element of NAT st CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),l))) = halt SCM+FSA holds
(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 <= l ;
then A34: LifeSpan ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 by A24, A25, EXTPRO_1:def 14;
A35: DataPart (Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))))) by A21, A15, EXTPRO_1:23, SCMFSA8A:60
.= DataPart (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))))) by A2, A23, A17, A20, Th11, A12, A1
.= DataPart (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) by EXTPRO_1:5
.= DataPart (Result ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))))) by A25, A34, EXTPRO_1:23 ;

A36: now

let x be set ; :: thesis: ( x in dom (IExec ((if=0 (a,I,J)),P,s)) implies (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b₁ )
A37: dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) = {(IC )} by FUNCOP_1:19;
A38: IExec ((if=0 (a,I,J)),P,s) = (Result ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1;
A39: IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s) = (Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1;
assume A40: x in dom (IExec ((if=0 (a,I,J)),P,s)) ; :: thesis: (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,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 or x is Element of NAT ) by A40, SCMFSA6A:35;

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

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

end;

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

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

end;

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

then A46: x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A37, TARSKI:def 1;
A47: not x in dom (s | NAT) by A45, A10, COMPOS_1:def 12;
then A48: IC (Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) = IC (IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) by A39, A45, FUNCT_4:12
.= ((card I) + (card J)) + 1 by A15, A21, SCMFSA8A:61 ;
thus (IExec ((if=0 (a,I,J)),P,s)) . x = (Result ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))))) . x by A38, A47, FUNCT_4:12
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))) . x by A25, A34, EXTPRO_1:23
.= IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialize ((intloc 0) .--> 1))),2)),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))))) by A45, EXTPRO_1:5
.= (IC (Comput ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))))))) + 2 by A2, A23, A17, A20, Th11, A12, A1
.= (IC (Result ((P +* (((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))))) + 2 by A21, A15, EXTPRO_1:23, SCMFSA8A:60
.= (Start-At (((((card I) + (card J)) + 1) + 2),SCM+FSA)) . (IC ) by A48, FUNCOP_1:87
.= ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A45, A46, FUNCT_4:14 ; :: thesis: verum

end;

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

then x <> IC by COMPOS_1:3;
then A50: not x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A37, TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x = (s | NAT) . x by A38, A49, A10, FUNCT_4:14
.= (IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) . x by A39, A49, A10, FUNCT_4:14
.= ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A50, FUNCT_4:12 ; :: thesis: verum

end;

end;

end;

dom (IExec ((if=0 (a,I,J)),P,s)) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom ((IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) by PARTFUN1:def 4 ;
hence IExec ((if=0 (a,I,J)),P,s) = (IExec ((((J ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A36, FUNCT_1:9
.= ((IExec (J,P,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,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by FUNCT_4:122 ;
:: thesis: verum