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 I1 = I ';' (Stop SCM+FSA );
set s1 = s +* (Initialized (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 i = a =0_goto ((card J) + 3);
A1: (I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= s +* (Initialized (I ';' (Stop SCM+FSA ))) by FUNCT_4:26, SCMFSA6B:8;
A2: if=0 a,I,J = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )) by SCMFSA6A:67;
A3: 0 in dom (if=0 a,I,J) by Lm2;
if=0 a,I,J c= Initialized (if=0 a,I,J) by SCMFSA6A:26;
then dom (if=0 a,I,J) c= dom (Initialized (if=0 a,I,J)) by GRFUNC_1:8;
then A4: (s +* (Initialized (if=0 a,I,J))) . 0 = (Initialized (if=0 a,I,J)) . 0 by A3, FUNCT_4:14
.= (if=0 a,I,J) . 0 by A3, SCMFSA6A:50
.= a =0_goto ((card J) + 3) by Lm3 ;
IC SCM+FSA in dom (Initialized (if=0 a,I,J)) by SCMFSA6A:24;
then A5: 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 ;
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;
A6: 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 A5, A4, Y ;
A7: 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 A8: if=0 a,I,J c= s +* (Initialized (if=0 a,I,J)) by A7, XBOOLE_1:1;
A9: not a in dom (Initialized (if=0 a,I,J)) by SCMFSA6A:48;
A10: dom (s | NAT ) = NAT by SCMFSA8A:3;
assume s . a = 0 ; :: thesis:
then (s +* (Initialized (if=0 a,I,J))) . a = 0 by A9, FUNCT_4:12;
then A11: IC (Comput (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))),1) = (card J) + 3 by A6, SCMFSA_2:96;
A12: DataPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) = DataPart (s +* (Initialized (if=0 a,I,J))) by SCMFSA6A:39, SCMFSA6A:53;

A13: now

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

end;

now

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

end;

then A14: DataPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) = DataPart (Comput (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))),1) by A13, 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 SCMFSA7B:6
.= (card J) + (2 + 1) ;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if=0 a,I,J by A2, Lm1;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= s +* (Initialized (if=0 a,I,J)) by A8, XBOOLE_1:1;
then ProgramPart (ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3))) c= Comput (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))),1 by AMI_1:99;
then A15: ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= Comput (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))),1 by RELAT_1:209;
assume A16: I is_closed_on Initialized s ; :: thesis:
assume A17: I is_halting_on Initialized s ; :: thesis:
then A18: ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA ))) by A16, SCMFSA8A:55;
I ';' (Stop SCM+FSA ) is_closed_on Initialized s by A16, A17, SCMFSA8A:46;
then A19: I ';' (Stop SCM+FSA ) is_closed_on s +* (Initialized (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))),1) 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 (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 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),(LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) by AMI_1:51;
A20: 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 (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1)) = CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))),1)),(Comput (ProgramPart (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),(LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))))) by x, T
.= IncAddr (CurInstr (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),(LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))))),((card J) + 3) by A1, A19, A15, A11, A14, Th11
.= IncAddr (halt SCM+FSA ),((card J) + 3) by A18, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
then A21: 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:
assume A22: l < (LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1 ; :: thesis:
Z: (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;
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;
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 ;

suppose l = 0 ; :: thesis:

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 (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 A5, A4, Z, TX3, SCMFSA_2:48, SCMFSA_2:124; :: thesis:

end;

suppose l <> 0 ; :: thesis:

then consider n being Nat such that
A23: l = n + 1 by NAT_1:6;
assume 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))),l) = halt SCM+FSA ; :: thesis:
reconsider n = n 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) by AMI_1:123;
x: Comput (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))),(n + 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),n by AMI_1:51;
InsCode (CurInstr (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),n)) = InsCode (IncAddr (CurInstr (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),n)),((card J) + 3)) by SCMFSA_4:22
.= InsCode (CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))),1)),(Comput (ProgramPart (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),n)) by A1, A19, A15, A11, A14, Th11
.= 0 by A23, A24, x, T, SCMFSA_2:124 ;
then A25: CurInstr (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),n) = halt SCM+FSA by SCMFSA_2:122;
n < LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))) by A22, A23, XREAL_1:8;
hence contradiction by A18, A25, AMI_1:def 46; :: thesis:

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 (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1 <= l ;
then A26: LifeSpan (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))) = (LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1 by A20, A21, 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))),1) by AMI_1:123;
ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA ))) by A16, A17, SCMFSA8A:55;
then A27: DataPart (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),(LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))))) by 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))),1),(LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))))) by A1, A19, A15, A11, A14, Th11, T
.= DataPart (Comput (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J))),((LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1)) by AMI_1:51
.= DataPart (Result (ProgramPart (s +* (Initialized (if=0 a,I,J)))),(s +* (Initialized (if=0 a,I,J)))) by A21, A26, AMI_1:122 ;

A28: now

let x be set ; :: thesis:
A29: IExec (I ';' (Stop SCM+FSA )),s = (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) +* (s | NAT ) by SCMFSA6B:def 1;
A30: ( x in dom (s | NAT ) implies x is Element of NAT ) by RELAT_1:86;
A31: dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) = {(IC SCM+FSA )} by FUNCOP_1:19;
A32: 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;
assume A33: x in dom (IExec (if=0 a,I,J),s) ; :: thesis:

per cases by A33, SCMFSA6A:35;

suppose A34: x is Int-Location ; :: thesis:

then x <> IC SCM+FSA by SCMFSA_2:81;
then A35: not x in dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A31, 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 A32, A30, A34, FUNCT_4:12, SCMFSA_2:84
.= (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) . x by A27, A34, SCMFSA6A:38
.= (IExec (I ';' (Stop SCM+FSA )),s) . x by A29, A30, A34, FUNCT_4:12, SCMFSA_2:84
.= ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . x by A35, FUNCT_4:12 ; :: thesis:

end;

suppose A36: x is FinSeq-Location ; :: thesis:

then x <> IC SCM+FSA by SCMFSA_2:82;
then A37: not x in dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A31, 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 A32, A30, A36, FUNCT_4:12, SCMFSA_2:85
.= (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) . x by A27, A36, SCMFSA6A:38
.= (IExec (I ';' (Stop SCM+FSA )),s) . x by A29, A30, A36, FUNCT_4:12, SCMFSA_2:85
.= ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . x by A37, FUNCT_4:12 ; :: thesis:

end;

suppose A38: x = IC SCM+FSA ; :: thesis:

then A39: x in dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A31, TARSKI:def 1;
A40: IC (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) = (IExec (I ';' (Stop SCM+FSA )),s) . (IC SCM+FSA ) by A29, A30, A38, COMPOS_1:3, FUNCT_4:12
.= IC ((IExec I,s) +* (Start-At (card I),SCM+FSA )) by A16, A17, SCMFSA8A:57
.= card I by FUNCT_4:121 ;
X: ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA ))) by A16, A17, SCMFSA8A:55;
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;
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 A32, A30, A38, 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 (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1)) . x by A21, A26, 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))),1),(LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))))) by A38, AMI_1:51
.= (IC (Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),(LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))))) + ((card J) + 3) by A1, A19, A15, A11, A14, Th11, T
.= (IC (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))))) + ((card J) + 3) by X, AMI_1:122
.= (Start-At ((card I) + ((card J) + 3)),SCM+FSA ) . (IC SCM+FSA ) by A40, FUNCOP_1:87
.= ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . x by A38, A39, FUNCT_4:14 ; :: thesis:

end;

suppose A41: x is Element of NAT ; :: thesis:

then x <> IC SCM+FSA by COMPOS_1:3;
then A42: not x in dom (Start-At (((card I) + (card J)) + 3),SCM+FSA ) by A31, TARSKI:def 1;
A43: x in NAT by A41;
hence (IExec (if=0 a,I,J),s) . x = (s | NAT ) . x by A10, A32, FUNCT_4:14
.= (IExec (I ';' (Stop SCM+FSA )),s) . x by A10, A29, A43, FUNCT_4:14
.= ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA )) . x by A42, FUNCT_4:12 ;
:: thesis:

end;

end;

end;

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