let P be Instruction-Sequence of SCM+FSA; :: thesis:
let s be 0 -started State of SCM+FSA; :: thesis:
let I be really-closed keeping_0 Program of ; :: thesis:
assume A1: P +* I halts_on s ; :: thesis:
let J be really-closed Program of ; :: thesis:
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 S₁[ 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:
then A3: P +* (I ";" J) = P by FUNCT_4:98;
A4: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let k be Nat; :: thesis:
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:
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 SCMFSA6A:38;
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 ;
IC ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))) = 0 by MEMSTR_0:def 11;
then A11: IC ((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))) in dom J by AFINSQ_1:65;
J c= (P +* I) +* J by FUNCT_4:25;
then A12: IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)) in dom J by AMISTD_1:21, A11;
then A13: 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 A14: (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 A12, COMPOS_1:def 21 ;
dom (Shift ((IncAddr (J,(card I))),(card I))) = { (il + (card I)) where il is Nat : il in dom (IncAddr (J,(card I))) } by VALUED_1:def 12;
then A15: ii + (card I) in dom (Shift ((IncAddr (J,(card I))),(card I))) by A13;
A16: J c= (P +* I) +* J by FUNCT_4:25;
A17: J /. ii = J . ii by A12, 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 A14, A16, A17, A12, GRFUNC_1:2
.= CurInstr ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) by A10, A8, A15, GRFUNC_1:2 ; :: thesis:

end;

A18: 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 A19: 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;
A20: 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 A19, A18, EXTPRO_1:3;
A21: 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 A19, A18, 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 A19, A18, FUNCT_4:113;
hence S₁[k + 1] by A20, A21, SCMFSA_2:61; :: thesis:

end;

A22: Directed I c= I ";" J by SCMFSA6A:16;

A23: now :: thesis:

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, A22, Th11, A3, A2, XBOOLE_1:1 ; :: thesis:
A24: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) by A1, A22, Th12, A2, XBOOLE_1:1;
set o = LifeSpan ((P +* I),s);

hereby :: thesis:

let a be Int-Location; :: thesis:
A25: 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 A25, 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 Th14, A1
.= (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a by A24, A3, SCMFSA_M:2 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
A26: 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 A26, 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 Th14, A1
.= (Comput ((P +* (I ";" J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f by A24, A3, SCMFSA_M:2 ;
:: thesis:

end;

A27: S₁[ 0 ] by A23, SCMFSA_2:61;
for k being Nat holds S₁[k] from NAT_1:sch 2(A27, 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: