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 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: 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;
A7: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[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 A8: 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: S₁[k + 1]
A9: 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

A10: I ';' J c= P +* (I ';' J) by FUNCT_4:25;
Reloc (J,(card I)) c= I ';' J by FUNCT_4:25;
then A11: Reloc (J,(card I)) c= P +* (I ';' J) by A10, XBOOLE_1:1;
B12: dom (P +* (I ';' J)) = NAT by PARTFUN1:def 2;
A13: 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 A8, B12, 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 ;
A14: Reloc (J,(card I)) = Shift ((IncAddr (J,(card I))),(card I)) by COMPOS_1:34;
J c= (P +* I) +* J by FUNCT_4:25;
then A16: IC (Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),k)) in dom J by AMISTD_1:def 10;
then A17: 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 19;
then A18: (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 A16, COMPOS_1:def 19 ;
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 A19: ii + (card I) in dom (Shift ((IncAddr (J,(card I))),(card I))) by A17;
A20: J c= (P +* I) +* J by FUNCT_4:25;
A21: J /. ii = J . ii by A16, 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 A18, A14, A20, A21, A16, GRFUNC_1:2
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),s,(((LifeSpan ((P +* I),s)) + 1) + k)))) by A13, A11, A14, A19, GRFUNC_1:2 ; :: thesis: verum

end;

A23: 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 A9, A8, 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 A24: 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;
A25: 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 A24, A23, EXTPRO_1:3;
A26: 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 A24, A23, 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 A24, A23, FUNCT_4:113;
hence S₁[k + 1] by A25, A26, SCMFSA_2:61; :: thesis: verum

end;

B29: Directed I c= I ';' J by SCMFSA6A:16;

A31: now

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, B29, Th37, 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 ) )
A32: DataPart (Comput (P,s,(LifeSpan ((P +* I),s)))) = DataPart (Comput (P,s,((LifeSpan ((P +* I),s)) + 1))) by A1, B29, Th38, 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
A34: 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 A34, 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 Th40, A1
.= (Comput ((P +* (I ';' J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . a by A32, A3, SCMFSA6A:7 ;
:: 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
A35: 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 A35, 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 Th40, A1
.= (Comput ((P +* (I ';' J)),s,(((LifeSpan ((P +* I),s)) + 1) + 0))) . f by A32, A3, SCMFSA6A:7 ;
:: thesis: verum

end;

Comput (((P +* I) +* J),((Result ((P +* I),s)) +* (Start-At (0,SCM+FSA))),0) = (Result ((P +* I),s)) +* (Start-At (0,SCM+FSA)) by EXTPRO_1:2;
then A37: S₁[ 0 ] by A31, SCMFSA_2:61;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A37, A7);
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