let s be State of SCM+FSA; :: thesis:
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let I be keeping_0 Program of SCM+FSA; :: thesis:
assume A1: P +* I halts_on s +* I ; :: thesis:
set ISA0 = Initialize I;
let J be paraclosed Program of SCM+FSA; :: thesis:
set sISA0 = s +* (Initialize I);
set RI = Result ((P +* I),(s +* (Initialize I)));
set JSA0 = Initialize J;
set RIJ = (Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J);
set sIJSA0 = s +* (Initialize (I ';' J));
defpred S₁[ Nat] means (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),$1)) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),$1))) + (card I)),SCM+FSA)), Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + $1)) equal_outside NAT ;
assume A2: I ';' J c= P ; :: thesis:
then A3: P +* (I ';' J) = P by FUNCT_4:79;
assume Initialize (I ';' J) c= s ; :: thesis:
then A4: s = s +* (Initialize (I ';' J)) by FUNCT_4:79;
A5: s +* (Initialize (I ';' J)) = Initialize (s +* (I ';' J)) by FUNCT_4:15;
s +* (Initialize (I ';' J)) = (Initialize s) +* (I ';' J) by A5, COMPOS_1:83;
then A6: I ';' J c= s by A4, FUNCT_4:26;
A7: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let k be Element of NAT ; :: thesis:
set k1 = k + 1;
set CRk = Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k);
set CRSk = IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)),(card I));
set CIJk = Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k));
set CRk1 = Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1));
set CRSk1 = (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1)))) + (card I)),SCM+FSA));
set CIJk1 = Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + (k + 1)));
assume A8: (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k))) + (card I)),SCM+FSA)), Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k)) equal_outside NAT ; :: thesis:
A9: IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))),(card I)) = CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k))))

proof

A10: I ';' J c= P +* (I ';' J) by FUNCT_4:26;
Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
then A11: Reloc (J,(card I)) c= P +* (I ';' J) by A10, XBOOLE_1:1;
dom (P +* (I ';' J)) = NAT by PARTFUN1:def 4;
then A12: (P +* (I ';' J)) /. (IC (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k)))) = (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k)))) by PARTFUN1:def 8;
A13: CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k)))) = (P +* (I ';' J)) . (IC (IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)),(card I)))) by A8, A12, COMPOS_1:24
.= (P +* (I ';' J)) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k))) + (card I)) by FUNCT_4:121 ;
reconsider ii = IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)) as Element of NAT ;
A14: Reloc (J,(card I)) = Shift ((IncAddr (J,(card I))),(card I)) by COMPOS_1:121;
A15: Initialize J c= (Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J) by FUNCT_4:26;
J c= (P +* I) +* J by FUNCT_4:26;
then A16: IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)) in dom J by Def2, A15;
then A17: IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)) in dom (IncAddr (J,(card I))) by COMPOS_1:def 40;
then A18: (Shift ((IncAddr (J,(card I))),(card I))) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k))) + (card I)) = (IncAddr (J,(card I))) . ii by VALUED_1:def 12
.= IncAddr ((J /. ii),(card I)) by A16, COMPOS_1:def 40 ;
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:26;
A21: J /. ii = J . ii by A16, PARTFUN1:def 8;
thus IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))),(card I)) = IncAddr ((((P +* I) +* J) . (IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))),(card I)) by PBOOLE:158
.= (Reloc (J,(card I))) . ((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k))) + (card I)) by A18, A14, A20, A21, A16, GRFUNC_1:8
.= CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k)))) by A13, A11, A14, A19, GRFUNC_1:8 ; :: thesis:

end;

A22: Exec ((IncAddr ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))),(card I))),(IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)),(card I)))) = IncIC ((Exec ((CurInstr (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))),(card I)) by AMISTD_5:4;
Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k)), IncIC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)),(card I)) equal_outside NAT by A8, FUNCT_7:28;
then A23: Exec ((CurInstr ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k))))),(Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k)))), IncIC ((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))),(card I)) equal_outside NAT by A22, A9, AMISTD_2:def 20;
Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + (k + 1))) = Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),((((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k) + 1)) ;
then A24: Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + (k + 1))) = Following ((P +* (I ';' J)),(Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + k)))) by EXTPRO_1:4;

A25: now

let a be Int-Location ; :: thesis:
thus ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1)))) + (card I)),SCM+FSA))) . a = (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1))) . a by SCMFSA_3:11
.= (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))) . a by EXTPRO_1:4
.= ((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))) +* (Start-At (((IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k))))) + (card I)),SCM+FSA))) . a by SCMFSA_3:11
.= (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + (k + 1)))) . a by A24, A23, SCMFSA10:92 ; :: thesis:

end;

A26: now

let f be FinSeq-Location ; :: thesis:
thus ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1)))) + (card I)),SCM+FSA))) . f = (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1))) . f by SCMFSA_3:12
.= (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))) . f by EXTPRO_1:4
.= ((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))) +* (Start-At (((IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k))))) + (card I)),SCM+FSA))) . f by SCMFSA_3:12
.= (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + (k + 1)))) . f by A24, A23, SCMFSA10:93 ; :: thesis:

end;

IC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1)))) + (card I)),SCM+FSA))) = (IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1)))) + (card I) by FUNCT_4:121
.= (IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k))))) + (card I) by EXTPRO_1:4 ;
then IC ((Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1))) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),(k + 1)))) + (card I)),SCM+FSA))) = IC ((Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k)))) +* (Start-At (((IC (Following (((P +* I) +* J),(Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),k))))) + (card I)),SCM+FSA))) by FUNCT_4:121
.= IC (Comput ((P +* (I ';' J)),(s +* (Initialize (I ';' J))),(((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + (k + 1)))) by A24, A23, COMPOS_1:24 ;
hence S₁[k + 1] by A25, A26, SCMFSA10:91; :: thesis:

end;

A27: s +* (Initialize I) = Initialize (s +* I) by FUNCT_4:15
.= (Initialize s) +* I by COMPOS_1:83
.= s +* I by A5, A4 ;
A28: Directed I c= I ';' J by SCMFSA6A:55;
then A29: Directed I c= P by XBOOLE_1:1, A2;
A30: Directed I c= s by A6, XBOOLE_1:1, A28;

A31: now

hereby :: thesis:

end;

end;

A36: s +* (Initialize (I ';' J)) = Initialize (s +* (I ';' J)) by FUNCT_4:15
.= (Initialize s) +* (I ';' J) by COMPOS_1:83
.= s +* (I ';' J) by A5, A4 ;
Comput (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J)),0) = (Result ((P +* I),(s +* (Initialize I)))) +* (Initialize J) by EXTPRO_1:3;
then A37: S₁[ 0 ] by A31, SCMFSA10:91;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A37, A7);
hence for k being Element of NAT holds (Comput (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialize J)),k)) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialize J)),k))) + (card I)),SCM+FSA)), Comput ((P +* (I ';' J)),(s +* (I ';' J)),(((LifeSpan ((P +* I),(s +* I))) + 1) + k)) equal_outside NAT by A27, A36; :: thesis: