let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let s be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,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 st s . a = 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let a be read-write Int-Location ; :: thesis: ( s . a = 0 & I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
set I1 = I ';' (Stop SCM+FSA);
set s1 = s +* (Initialized (I ';' (Stop SCM+FSA)));
set P1 = P +* (I ';' (Stop SCM+FSA));
A1: I ';' (Stop SCM+FSA) c= P +* (I ';' (Stop SCM+FSA)) by FUNCT_4:26;
set s3 = s +* (Initialized (if=0 (a,I,J)));
set P3 = P +* (if=0 (a,I,J));
set s4 = Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1);
set i = a =0_goto ((card J) + 3);
A2: Initialize (I ';' (Stop SCM+FSA)) c= s +* (Initialized (I ';' (Stop SCM+FSA))) by FUNCT_4:26, SCMFSA6B:8;
A3: if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA)) by SCMFSA6A:67;
A4: 0 in dom (if=0 (a,I,J)) by Lm2;
A5: (P +* (if=0 (a,I,J))) . 0 = (if=0 (a,I,J)) . 0 by A4, FUNCT_4:14
.= a =0_goto ((card J) + 3) by Lm3 ;
IC in dom (Initialized (if=0 (a,I,J))) by SCMFSA6A:24;
then A6: IC (s +* (Initialized (if=0 (a,I,J)))) = (Initialized (if=0 (a,I,J))) . (IC ) by FUNCT_4:14
.= 0 by SCMFSA6A:46 ;
A7: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),(0 + 1)) = Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),0))) by EXTPRO_1:4
.= Following ((P +* (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 A6, A5, PBOOLE:158 ;
A8: if=0 (a,I,J) c= Initialized (if=0 (a,I,J)) by SCMFSA6A:26;
Initialized (if=0 (a,I,J)) c= s +* (Initialized (if=0 (a,I,J))) by FUNCT_4:26;
then A9: if=0 (a,I,J) c= s +* (Initialized (if=0 (a,I,J))) by A8, XBOOLE_1:1;
A10: if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:26;
A11: not a in dom (Initialized (if=0 (a,I,J))) by SCMFSA6A:48;
A12: dom (ProgramPart s) = NAT by COMPOS_1:34;
assume s . a = 0 ; :: thesis: ( not I is_closed_on Initialized s,P or not I is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
then (s +* (Initialized (if=0 (a,I,J)))) . a = 0 by A11, FUNCT_4:12;
then A13: IC (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)) = (card J) + 3 by A7, SCMFSA_2:96;
A14: DataPart (s +* (Initialized (I ';' (Stop SCM+FSA)))) = DataPart (s +* (Initialized (if=0 (a,I,J)))) by COMPOS_1:138, SCMFSA6A:53;

A15: now

let f be FinSeq-Location ; :: thesis: (s +* (Initialized (I ';' (Stop SCM+FSA)))) . f = (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)) . f
thus (s +* (Initialized (I ';' (Stop SCM+FSA)))) . f = (s +* (Initialized (if=0 (a,I,J)))) . f by A14, SCMFSA6A:38
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)) . f by A7, SCMFSA_2:96 ; :: thesis: verum

end;

now

let a be Int-Location ; :: thesis: (s +* (Initialized (I ';' (Stop SCM+FSA)))) . a = (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)) . a
thus (s +* (Initialized (I ';' (Stop SCM+FSA)))) . a = (s +* (Initialized (if=0 (a,I,J)))) . a by A14, SCMFSA6A:38
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)) . a by A7, SCMFSA_2:96 ; :: thesis: verum

end;

then A16: DataPart (s +* (Initialized (I ';' (Stop SCM+FSA)))) = DataPart (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)) by A15, SCMFSA6A:38;
card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) = card (((Macro (a =0_goto ((card J) + 3))) ';' J) ';' (Goto ((card I) + 1))) by SCMFSA6A:def 6
.= (card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1))) by SCMFSA6A:61
.= (card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + 1 by SCMFSA8A:29
.= ((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1 by SCMFSA6A:61
.= ((card J) + 2) + 1 by COMPOS_1:150
.= (card J) + (2 + 1) ;
then A17: Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= if=0 (a,I,J) by A3, Lm1;
then Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= s +* (Initialized (if=0 (a,I,J))) by A9, XBOOLE_1:1;
then A18: Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1) by AMI_1:81;
A19: Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= P +* (if=0 (a,I,J)) by A17, A10, XBOOLE_1:1;
assume A20: I is_closed_on Initialized s,P ; :: thesis: ( not I is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
assume A21: I is_halting_on Initialized s,P ; :: thesis: IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
then A22: P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialized (I ';' (Stop SCM+FSA))) by A20, SCMFSA8A:55;
I ';' (Stop SCM+FSA) is_closed_on Initialized s,P by A20, A21, SCMFSA8A:46;
then A23: I ';' (Stop SCM+FSA) is_closed_on s +* (Initialized (I ';' (Stop SCM+FSA))),P +* (I ';' (Stop SCM+FSA)) by Th9;
A24: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 1)))) = CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA))))))))) by EXTPRO_1:5
.= IncAddr ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))))))),((card J) + 3)) by A2, A23, A18, A13, A16, Th11, A19, A1
.= IncAddr ((halt SCM+FSA),((card J) + 3)) by A22, EXTPRO_1:def 14
.= halt SCM+FSA by COMPOS_1:93 ;
then A25: P +* (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 ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 1 implies CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),b₁))) <> halt SCM+FSA )
assume A26: l < (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 1 ; :: thesis: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),b₁))) <> halt SCM+FSA
A27: Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),0) = s +* (Initialized (if=0 (a,I,J))) by EXTPRO_1:3;

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

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

hence CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),l))) <> halt SCM+FSA by A6, A5, PBOOLE:158, A27; :: thesis: verum

end;

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

then consider n being Nat such that
A28: l = n + 1 by NAT_1:6;
assume A29: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),l))) = halt SCM+FSA ; :: thesis: contradiction
reconsider n = n as Element of NAT by ORDINAL1:def 13;
InsCode (CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),n)))) = InsCode (IncAddr ((CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),n)))),((card J) + 3))) by COMPOS_1:def 38
.= InsCode (CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)),n)))) by A2, A23, A18, A13, A16, Th11, A19, A1
.= 0 by A28, A29, EXTPRO_1:5, SCMFSA_2:124 ;
then A30: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),n))) = halt SCM+FSA by SCMFSA_2:122;
n < LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA))))) by A26, A28, XREAL_1:8;
hence contradiction by A22, A30, 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 +* (Initialized (if=0 (a,I,J)))),l))) = halt SCM+FSA holds
(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 1 <= l ;
then A31: LifeSpan ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J))))) = (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 1 by A24, A25, EXTPRO_1:def 14;
A32: DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))))) by EXTPRO_1:23, A20, A21, SCMFSA8A:55
.= DataPart (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))))) by A2, A23, A18, A13, A16, Th11, A1, A19
.= DataPart (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 1))) by EXTPRO_1:5
.= DataPart (Result ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))))) by A25, A31, EXTPRO_1:23 ;

A33: 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 ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b₁ )
A34: IExec ((I ';' (Stop SCM+FSA)),P,s) = (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) +* (s | NAT) by SCMFSA6B:def 1;
A35: dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) = {(IC )} by FUNCOP_1:19;
A36: IExec ((if=0 (a,I,J)),P,s) = (Result ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))))) +* (s | NAT) by SCMFSA6B:def 1;
A37: dom (ProgramPart s) = NAT by COMPOS_1:34;
assume A38: x in dom (IExec ((if=0 (a,I,J)),P,s)) ; :: thesis: (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((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 A38, SCMFSA6A:35;

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

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

end;

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

then x <> IC by SCMFSA_2:82;
then A42: not x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A35, TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x = (Result ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))))) . x by A36, FUNCT_4:12, A41, SCMFSA10:4, A37
.= (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) . x by A32, A41, SCMFSA6A:38
.= (IExec ((I ';' (Stop SCM+FSA)),P,s)) . x by A34, FUNCT_4:12, A41, SCMFSA10:4, A37
.= ((IExec ((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 = IC ; :: thesis: (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b₁

then A44: x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A35, TARSKI:def 1;
A45: not x in dom (s | NAT) by A43, COMPOS_1:def 12, A37;
A46: IC (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) = (IExec ((I ';' (Stop SCM+FSA)),P,s)) . (IC ) by A34, A43, FUNCT_4:12, A45
.= IC ((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))) by A20, A21, SCMFSA8A:57
.= card I by FUNCT_4:121 ;
thus (IExec ((if=0 (a,I,J)),P,s)) . x = (Result ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))))) . x by A36, FUNCT_4:12, A45
.= (Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),((LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 1))) . x by A25, A31, EXTPRO_1:23
.= IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(s +* (Initialized (if=0 (a,I,J)))),1)),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))))) by A43, EXTPRO_1:5
.= (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),(LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA))))))))) + ((card J) + 3) by A2, A23, A18, A13, A16, Th11, A19, A1
.= (IC (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA))))))) + ((card J) + 3) by A20, A21, SCMFSA8A:55, EXTPRO_1:23
.= (Start-At (((card I) + ((card J) + 3)),SCM+FSA)) . (IC ) by A46, FUNCOP_1:87
.= ((IExec ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A43, A44, FUNCT_4:14 ; :: thesis: verum

end;

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

then x <> IC by COMPOS_1:3;
then A48: not x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A35, TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x = (s | NAT) . x by A36, FUNCT_4:14, A47, A12
.= (IExec ((I ';' (Stop SCM+FSA)),P,s)) . x by A34, A47, FUNCT_4:14, A12
.= ((IExec ((I ';' (Stop SCM+FSA)),P,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)),P,s)) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom ((IExec ((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 ((I ';' (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A33, FUNCT_1:9
.= ((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A20, A21, SCMFSA8A:57
.= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by FUNCT_4:122 ;
:: thesis: verum