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 & I is_closed_on Initialized s & I is_halting_on Initialized s holds
IExec ((if>0 (a,I,J)),s) = (IExec (I,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 & I is_closed_on Initialized s & I is_halting_on Initialized s holds
IExec ((if>0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let s be State of SCM+FSA; :: thesis: ( s . a > 0 & I is_closed_on Initialized s & I is_halting_on Initialized s implies IExec ((if>0 (a,I,J)),s) = (IExec (I,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 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 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 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 (ProgramPart s) = NAT by COMPOS_1:34;
assume s . a > 0 ; :: thesis: ( not I is_closed_on Initialized s or not I is_halting_on Initialized s or IExec ((if>0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
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:97;
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: (s +* (Initialized (I ';' (Stop SCM+FSA)))) . f = (Comput ((ProgramPart (s +* (Initialized (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 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:97 ; :: thesis: verum
end;
now
let a be Int-Location ; :: thesis: (s +* (Initialized (I ';' (Stop SCM+FSA)))) . a = (Comput ((ProgramPart (s +* (Initialized (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 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:97 ; :: thesis: verum
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 COMPOS_1:150
.= (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: ( not I is_halting_on Initialized s or IExec ((if>0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
assume A17: I is_halting_on Initialized s ; :: thesis: IExec ((if>0 (a,I,J)),s) = (IExec (I,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
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 EXTPRO_1:5;
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, EXTPRO_1:def 14
.= 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 EXTPRO_1:30;
now
let l be Element of NAT ; :: thesis: ( l < (LifeSpan ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 1 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)))),b1))) <> halt SCM+FSA )
assume A22: l < (LifeSpan ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) + 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)))),b1))) <> 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;
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;
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;
per cases ( l = 0 or l <> 0 ) ;
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)))),b1))) <> 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 A5, A4, Z; :: thesis: verum
end;
suppose l <> 0 ; :: 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)))),b1))) = halt SCM+FSA
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: contradiction
reconsider n = n 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)))),(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 EXTPRO_1:5;
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, 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 (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, 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)))),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 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)))),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 EXTPRO_1:5
.= DataPart (Result ((ProgramPart (s +* (Initialized (if>0 (a,I,J))))),(s +* (Initialized (if>0 (a,I,J)))))) by A21, A26, EXTPRO_1:23 ;
A28: now
let x be set ; :: thesis: ( x in dom (IExec ((if>0 (a,I,J)),s)) implies (IExec ((if>0 (a,I,J)),s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1 )
A29: ( x in dom (s | NAT) implies x is Element of NAT ) by RELAT_1:86;
A30: dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) = {(IC SCM+FSA)} by FUNCOP_1:19;
A31: 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;
A32: 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;
assume A33: x in dom (IExec ((if>0 (a,I,J)),s)) ; :: thesis: (IExec ((if>0 (a,I,J)),s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1
per cases ( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Element of NAT ) by A33, SCMFSA6A:35;
suppose A34: x is Int-Location ; :: thesis: (IExec ((if>0 (a,I,J)),s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1
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 A30, 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 A29, A31, 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, A32, 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: verum
end;
suppose A36: x is FinSeq-Location ; :: thesis: (IExec ((if>0 (a,I,J)),s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1
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 A30, 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 A29, A31, 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, A32, 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: verum
end;
suppose A38: x = IC SCM+FSA ; :: thesis: (IExec ((if>0 (a,I,J)),s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1
then A39: x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A30, 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, A32, 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 ;
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: ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA)))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA))) by A16, A17, SCMFSA8A:55;
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 A29, A31, 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, 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)))),1)),(LifeSpan ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))))) by A38, EXTPRO_1:5
.= (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, EXTPRO_1:23
.= (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: verum
end;
suppose A41: x is Element of NAT ; :: thesis: (IExec ((if>0 (a,I,J)),s)) . b1 = ((IExec ((I ';' (Stop SCM+FSA)),s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b1
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 A30, TARSKI:def 1;
A43: x in NAT by A41;
hence (IExec ((if>0 (a,I,J)),s)) . x = (s | NAT) . x by A10, A31, FUNCT_4:14
.= (IExec ((I ';' (Stop SCM+FSA)),s)) . x by A10, A32, 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: verum
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: verum