let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being 0 -started State of SCM+FSA
for I being keeping_0 Program of st P +* I halts_on s holds
for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
let s be 0 -started State of SCM+FSA; :: thesis: for I being keeping_0 Program of st P +* I halts_on s holds
for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
let I be keeping_0 Program of ; :: thesis: ( P +* I halts_on s implies for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)) )
assume A1: P +* I halts_on s ; :: thesis: for J being paraclosed Program of st I ";" J c= P holds
for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
let J be paraclosed Program of ; :: thesis: ( I ";" J c= P implies for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)) )
set RI = Result ((P +* I),s);
set JSA0 = Start-At (0,SCM+FSA);
set RIJ = (Result ((P +* I),s)) +* (Start-At (0,SCM+FSA));
defpred S1[ Nat] means IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),$1)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + $1));
assume A2: I ";" J c= P ; :: thesis: for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))
then A3: P +* (I ";" J) = P by FUNCT_4:98;
A4: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
set k1 = k + 1;
set CRk = Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k);
set CRSk = IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I));
set CIJk = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k));
set CRk1 = Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1));
set CRSk1 = IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I));
set CIJk1 = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1)));
assume A5: IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)) ; :: thesis: S1[k + 1]
A6: IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)))),(card I)) = CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))))
proof
A7: I ";" J c= P +* (I ";" J) by FUNCT_4:25;
Reloc (J,(card I)) c= I ";" J by FUNCT_4:25;
then A8: Reloc (J,(card I)) c= P +* (I ";" J) by A7, XBOOLE_1:1;
A9: dom (P +* (I ";" J)) = NAT by PARTFUN1:def 2;
A10: CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = (P +* (I ";" J)) . (IC (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)),(card I)))) by A5, A9, PARTFUN1:def 6
.= (P +* (I ";" J)) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k))) + (card I)) by FUNCT_4:113 ;
reconsider ii = IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)) as Element of NAT ;
J c= (P +* I) +* J by FUNCT_4:25;
then A11: IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)) in dom J by AMISTD_1:def 10;
then A12: IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)) in dom (IncAddr (J,(card I))) by COMPOS_1:def 21;
then A13: (Shift ((IncAddr (J,(card I))),(card I))) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k))) + (card I)) = (IncAddr (J,(card I))) . ii by VALUED_1:def 12
.= IncAddr ((J /. ii),(card I)) by A11, COMPOS_1:def 21 ;
dom (Shift ((IncAddr (J,(card I))),(card I))) = { (il + (card I)) where il is Element of NAT : il in dom (IncAddr (J,(card I))) } by VALUED_1:def 12;
then A14: ii + (card I) in dom (Shift ((IncAddr (J,(card I))),(card I))) by A12;
A15: J c= (P +* I) +* J by FUNCT_4:25;
A16: J /. ii = J . ii by A11, PARTFUN1:def 6;
thus IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)))),(card I)) = IncAddr ((((P +* I) +* J) . (IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)))),(card I)) by PBOOLE:143
.= (Reloc (J,(card I))) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k))) + (card I)) by A13, A15, A16, A11, GRFUNC_1:2
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) by A10, A8, A14, GRFUNC_1:2 ; :: thesis: verum
end;
A17: Exec ((CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k))))),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) = IncIC ((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)))),(card I)) by A6, A5, AMISTD_5:4;
Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1))) = Comput ((P +* (I ";" J)),s,((((LifeSpan ((P +* I),s)) + 1) + k) + 1)) ;
then A18: Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1))) = Following ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) by EXTPRO_1:3;
A19: for a being Int-Location holds (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I))) . a = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1)))) . a by A18, A17, EXTPRO_1:3;
A20: for f being FinSeq-Location holds (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1)))) . f by A18, A17, EXTPRO_1:3;
IC (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I))) = (IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1)))) + (card I) by FUNCT_4:113
.= (IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k))))) + (card I) by EXTPRO_1:3 ;
then IC (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(k + 1))),(card I))) = IC (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + (k + 1)))) by A18, A17, FUNCT_4:113;
hence S1[k + 1] by A19, A20, SCMFSA_2:61; :: thesis: verum
end;
A21: Directed I c= I ";" J by SCMFSA6A:16;
A22: now :: thesis: ( IC (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) = IC (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) & ( for a being Int-Location holds (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . a = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a ) & ( for f being FinSeq-Location holds (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f ) )
set s2 = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0));
set s1 = IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I));
thus IC (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) = (IC ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA)))) + (card I) by FUNCT_4:113
.= 0 + (card I) by FUNCT_4:113
.= IC (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) by A1, A21, Th13, A3, A2, XBOOLE_1:1 ; :: thesis: ( ( for a being Int-Location holds (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . a = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a ) & ( for f being FinSeq-Location holds (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f ) )
A23: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) by A1, A21, Th14, A2, XBOOLE_1:1;
set o = LifeSpan ((P +* I),s);
hereby :: thesis: for f being FinSeq-Location holds (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f
let a be Int-Location; :: thesis: (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . a = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a
A24: not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
not a in dom (Start-At (((IC ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA)) by SCMFSA_2:102;
hence (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . a = ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))) . a by FUNCT_4:11
.= (Result ((P +* I),s)) . a by A24, FUNCT_4:11
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . a by A1, EXTPRO_1:23
.= (Comput ((P +* (I ";" J)),s,(LifeSpan ((P +* I),s)))) . a by Th16, A1
.= (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a by A23, A3, SCMFSA_M:2 ;
:: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f
A25: not f in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:103;
not f in dom (Start-At (((IC ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA)))) + (card I)),SCM+FSA)) by SCMFSA_2:103;
hence (IncIC (((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),(card I))) . f = ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))) . f by FUNCT_4:11
.= (Result ((P +* I),s)) . f by A25, FUNCT_4:11
.= (Comput ((P +* I),s,(LifeSpan ((P +* I),s)))) . f by A1, EXTPRO_1:23
.= (Comput ((P +* (I ";" J)),s,(LifeSpan ((P +* I),s)))) . f by Th16, A1
.= (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f by A23, A3, SCMFSA_M:2 ;
:: thesis: verum
end;
A26: S1[ 0 ] by A22, SCMFSA_2:61;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A26, A4);
 hence for k being Element of NAT holds IncIC ((Comput (((P +* I) +* J),(Initialize (Result ((P +* I),s))),k)),(card I)) = Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)) ; :: thesis: verum