let P be Instruction-Sequence of SCM+FSA; :: 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 = Initialized s;
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:25;
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),(Initialized s),1);
set s5 = Comput ((P +* (if>0 (a,I,J))),(Initialized s),2);
set i = a >0_goto ((card J) + 3);
0 in dom (if>0 (a,I,J)) by Lm2;
then A2: (P +* (if>0 (a,I,J))) . 0 = (if>0 (a,I,J)) . 0 by FUNCT_4:13
.= a >0_goto ((card J) + 3) by Lm3 ;
A3: 1 in dom (if>0 (a,I,J)) by Lm2;
A4: (P +* (if>0 (a,I,J))) . 1 = (if>0 (a,I,J)) . 1 by A3, FUNCT_4:13
.= goto 2 by Lm3 ;
A5: dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )} by SCMFSA_M:11;
( a <> intloc 0 & a <> IC ) by SCMFSA_2:56;
then A6: not a in dom (Initialize ((intloc 0) .--> 1)) by A5, TARSKI:def 2;
IC in dom (Initialize ((intloc 0) .--> 1)) by MEMSTR_0:48;
then A7: IC (Initialized s) = IC (Initialize ((intloc 0) .--> 1)) by FUNCT_4:13
.= 0 by MEMSTR_0:def 11 ;
if>0 (a,I,J) = (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= ((a >0_goto ((card J) + 3)) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= (a >0_goto ((card J) + 3)) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) by SCMFSA6A:29
.= (a >0_goto ((card J) + 3)) ";" ((J ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= (Macro (a >0_goto ((card J) + 3))) ";" (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)) by SCMFSA6A:25 ;
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:56;
if>0 (a,I,J) c= P +* (if>0 (a,I,J)) by FUNCT_4:25;
then A9: Reloc ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),2) c= P +* (if>0 (a,I,J)) by A8, XBOOLE_1:1;
A10: Comput ((P +* (if>0 (a,I,J))),(Initialized s),(0 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),0))) by EXTPRO_1:3
.= Following ((P +* (if>0 (a,I,J))),(Initialized s))
.= Exec ((a >0_goto ((card J) + 3)),(Initialized s)) by A7, A2, PBOOLE:143 ;
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 (Initialized s) . a <= 0 by A6, FUNCT_4:11;
then A11: IC (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) = succ 0 by A7, A10, SCMFSA_2:71
.= 0 + 1 ;
assume A12: 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)) )
A13: Comput ((P +* (if>0 (a,I,J))),(Initialized s),(1 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),1))) by A11, A4, PBOOLE:143 ;
then A14: IC (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) = 2 by SCMFSA_2:69;

A15: now :: thesis: for f being FinSeq-Location holds (Initialized s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . f

let f be FinSeq-Location ; :: thesis: (Initialized s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . f
thus (Initialized s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) . f by A10, SCMFSA_2:71
.= (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . f by A13, SCMFSA_2:69 ; :: thesis: verum

end;

now :: thesis: for a being Int-Location holds (Initialized s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . a

let a be Int-Location; :: thesis: (Initialized s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . a
thus (Initialized s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialized s),1)) . a by A10, SCMFSA_2:71
.= (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) . a by A13, SCMFSA_2:69 ; :: thesis: verum

end;

then A16: DataPart (Initialized s) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)) by A15, SCMFSA_M:2;
assume A17: 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 A18: P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)) halts_on Initialized s by A12, SCMFSA8A:39;
((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is_closed_on Initialized s,P by A12, A17, SCMFSA8A:37;
then A19: ((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is_closed_on Initialized s,P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)) by Th6;
A20: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 2)))) = CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s)))))) by EXTPRO_1:4
.= IncAddr ((CurInstr ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Comput ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))))))),2) by A19, A14, A16, Th8, A9, A1
.= IncAddr ((halt SCM+FSA),2) by A18, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
then A21: P +* (if>0 (a,I,J)) halts_on Initialized s by EXTPRO_1:29;

now :: thesis: for l being Element of NAT st l < (LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 2 holds
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l))) <> halt SCM+FSA

let l be Element of NAT ; :: thesis: ( l < (LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 2 implies CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),b₁))) <> halt SCM+FSA )
assume A22: l < (LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 2 ; :: thesis: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),b₁))) <> halt SCM+FSA
A23: Comput ((P +* (if>0 (a,I,J))),(Initialized s),0) = Initialized s ;

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))),(Initialized s),b₁))) <> halt SCM+FSA

hence CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l))) <> halt SCM+FSA by A7, A2, A23, PBOOLE:143; :: thesis: verum

end;

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

hence CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l))) <> halt SCM+FSA by A11, A4, PBOOLE:143; :: thesis: verum

end;

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

assume A25: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),l))) = halt SCM+FSA ; :: thesis: contradiction
consider n being Nat such that
A26: l = n + 1 by A24, NAT_1:6;
n <> 0 by A24, A26;
then consider l2 being Nat such that
A27: n = l2 + 1 by NAT_1:6;
reconsider l2 = l2 as Element of NAT by ORDINAL1:def 12;
InsCode (CurInstr ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Comput ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s),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))),(Initialized s),l2)))),2)) by COMPOS_0:def 9
.= InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)),l2)))) by A19, A14, A16, Th8, A9, A1
.= InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),(l2 + (1 + 1)))))) by EXTPRO_1:4
.= 0 by A26, A27, A25, COMPOS_1:70 ;
then A28: CurInstr ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Comput ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s),l2))) = halt SCM+FSA by SCMFSA_2:95;
n + 1 < ((LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 1) + 1 by A22, A26;
then n < (LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 1 by XREAL_1:6;
then l2 < LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s)) by A27, XREAL_1:6;
hence contradiction by A18, A28, EXTPRO_1:def 15; :: 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))),(Initialized s),l))) = halt SCM+FSA holds
(LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 2 <= l ;
then A29: LifeSpan ((P +* (if>0 (a,I,J))),(Initialized s)) = (LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 2 by A20, A21, EXTPRO_1:def 15;
A30: DataPart (Result ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Comput ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))))) by A17, A12, EXTPRO_1:23, SCMFSA8A:39
.= DataPart (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))))) by A19, A14, A16, Th8, A9, A1
.= DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 2))) by EXTPRO_1:4
.= DataPart (Result ((P +* (if>0 (a,I,J))),(Initialized s))) by A21, A29, EXTPRO_1:23 ;

A31: now :: thesis: for x being set st x in dom (IExec ((if>0 (a,I,J)),P,s)) holds
(IExec ((if>0 (a,I,J)),P,s)) . x = ((IExec ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x

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₁ )
A32: dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) = {(IC )} by FUNCOP_1:13;
A33: IExec ((if>0 (a,I,J)),P,s) = Result ((P +* (if>0 (a,I,J))),(Initialized s)) by SCMFSA6B:def 1;
A34: IExec ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),P,s) = Result ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s)) by SCMFSA6B:def 1;
assume A35: 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 ) by A35, SCMFSA_M:1;

suppose A36: 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:56;
then A37: not x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A32, TARSKI:def 1;
thus (IExec ((if>0 (a,I,J)),P,s)) . x = (Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x by A33
.= (Result ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) . x by A30, A36, SCMFSA_M:2
.= (IExec ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),P,s)) . x by A34
.= ((IExec ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A37, FUNCT_4:11 ; :: thesis: verum

end;

suppose A38: 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:57;
then A39: not x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A32, TARSKI:def 1;
thus (IExec ((if>0 (a,I,J)),P,s)) . x = (Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x by A33
.= (Result ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) . x by A30, A38, SCMFSA_M:2
.= (IExec ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),P,s)) . x by A34
.= ((IExec ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A39, FUNCT_4:11 ; :: thesis: verum

end;

suppose A40: 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 A41: x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A32, TARSKI:def 1;
A42: IC (Result ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) = IC (IExec ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),P,s)) by A34
.= ((card I) + (card J)) + 1 by A12, A17, SCMFSA8A:40 ;
thus (IExec ((if>0 (a,I,J)),P,s)) . x = (Result ((P +* (if>0 (a,I,J))),(Initialized s))) . x by A33
.= (Comput ((P +* (if>0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))) + 2))) . x by A21, A29, EXTPRO_1:23
.= IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialized s),2)),(LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s))))) by A40, EXTPRO_1:4
.= (IC (Comput ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s)))))) + 2 by A19, A14, A16, Th8, A9, A1
.= (IC (Result ((P +* (((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA))),(Initialized s)))) + 2 by A17, A12, EXTPRO_1:23, SCMFSA8A:39
.= (Start-At (((((card I) + (card J)) + 1) + 2),SCM+FSA)) . (IC ) by A42, FUNCOP_1:72
.= ((IExec ((((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A40, A41, FUNCT_4:13 ; :: thesis: verum

end;

end;

end;

dom (IExec ((if>0 (a,I,J)),P,s)) = the carrier of SCM+FSA by PARTFUN1:def 2
.= 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 2 ;
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 A31, FUNCT_1:2
.= ((IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A12, A17, SCMFSA8A:41
.= (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by FUNCT_4:114 ;
:: thesis: verum