let s1, s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I +* (Start-At (0,SCM+FSA)) c= s1 & I is_pseudo-closed_on s1 holds
for n being Element of NAT st ProgramPart (Relocated (I,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,I) holds
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) )
let I be Program of SCM+FSA; :: thesis: ( I +* (Start-At (0,SCM+FSA)) c= s1 & I is_pseudo-closed_on s1 implies for n being Element of NAT st ProgramPart (Relocated (I,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,I) holds
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) ) )
assume A1: I +* (Start-At (0,SCM+FSA)) c= s1 ; :: thesis: ( not I is_pseudo-closed_on s1 or for n being Element of NAT st ProgramPart (Relocated (I,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,I) holds
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) ) )
assume A2: I is_pseudo-closed_on s1 ; :: thesis: for n being Element of NAT st ProgramPart (Relocated (I,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,I) holds
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) )
let n be Element of NAT ; :: thesis: ( ProgramPart (Relocated (I,n)) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 implies ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,I) holds
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) ) )
assume A3: ProgramPart (Relocated (I,n)) c= s2 ; :: thesis: ( not IC s2 = n or not DataPart s1 = DataPart s2 or ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,I) holds
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) ) )
defpred S1[ Nat] means ( $1 <= pseudo-LifeSpan (s1,I) implies ( (IC (Comput ((ProgramPart s1),s1,$1))) + n = IC (Comput ((ProgramPart s2),s2,$1)) & DataPart (Comput ((ProgramPart s1),s1,$1)) = DataPart (Comput ((ProgramPart s2),s2,$1)) ) );
assume A4: IC s2 = n ; :: thesis: ( not DataPart s1 = DataPart s2 or ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,I) holds
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) ) )
assume A5: DataPart s1 = DataPart s2 ; :: thesis: ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,I) holds
IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) ) )
hereby :: thesis: for i being Element of NAT st i <= pseudo-LifeSpan (s1,I) holds
( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
defpred S2[ Nat] means ( $1 < pseudo-LifeSpan (s1,I) implies ( (IC (Comput ((ProgramPart s1),s1,$1))) + n = IC (Comput ((ProgramPart s2),s2,$1)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,$1))),(Comput ((ProgramPart s1),s1,$1)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,$1))),(Comput ((ProgramPart s2),s2,$1))) & DataPart (Comput ((ProgramPart s1),s1,$1)) = DataPart (Comput ((ProgramPart s2),s2,$1)) ) );
let i be Element of NAT ; :: thesis: ( i < pseudo-LifeSpan (s1,I) implies IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) )
assume A7: i < pseudo-LifeSpan (s1,I) ; :: thesis: IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i)))
A8: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
A9: I c= I +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A10: dom I c= dom (I +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A11: S2[k] ; :: thesis: S2[k + 1]
reconsider l = IC (Comput ((ProgramPart s1),s1,(k + 1))) as Element of NAT ;
reconsider j = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1)))) as Instruction of SCM+FSA ;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))) /. (IC (Comput ((ProgramPart s1),s1,(k + 1)))) = (Comput ((ProgramPart s1),s1,(k + 1))) . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by COMPOS_1:38;
assume A12: k + 1 < pseudo-LifeSpan (s1,I) ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,(k + 1)))) + n = IC (Comput ((ProgramPart s2),s2,(k + 1))) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1))))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))),(Comput ((ProgramPart s2),s2,(k + 1)))) & DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) )
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
A14: Comput ((ProgramPart s1),s1,(k + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))),(Comput ((ProgramPart s1),s1,k))) by T ;
s1 +* (I +* (Start-At (0,SCM+FSA))) = s1 by A1, FUNCT_4:79;
then A15: IC (Comput ((ProgramPart s1),s1,(k + 1))) in dom I by A2, A12, SCMFSA8A:def 5;
dom (ProgramPart I) = (dom I) /\ NAT by RELAT_1:90;
then A16: l in dom (ProgramPart I) by A15, XBOOLE_0:def 4;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,k)) by AMI_1:123;
A17: Comput ((ProgramPart s2),s2,(k + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,k))),(Comput ((ProgramPart s2),s2,k)))),(Comput ((ProgramPart s2),s2,k))) by T ;
A18: k + 0 < k + 1 by XREAL_1:8;
hence A19: (IC (Comput ((ProgramPart s1),s1,(k + 1)))) + n = IC (Comput ((ProgramPart s2),s2,(k + 1))) by A11, A12, A14, A17, SCMFSA6A:41, XXREAL_0:2; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1))))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))),(Comput ((ProgramPart s2),s2,(k + 1)))) & DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) )
then IC (Comput ((ProgramPart s2),s2,(k + 1))) in dom (Relocated (I,n)) by A15, COMPOS_1:118;
then IC (Comput ((ProgramPart s2),s2,(k + 1))) in (dom (Relocated (I,n))) /\ NAT by XBOOLE_0:def 4;
then A20: IC (Comput ((ProgramPart s2),s2,(k + 1))) in dom (ProgramPart (Relocated (I,n))) by RELAT_1:90;
Z: (ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))) /. (IC (Comput ((ProgramPart s2),s2,(k + 1)))) = (Comput ((ProgramPart s2),s2,(k + 1))) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by COMPOS_1:38;
j = s1 . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by Y, AMI_1:54
.= (I +* (Start-At (0,SCM+FSA))) . (IC (Comput ((ProgramPart s1),s1,(k + 1)))) by A1, A10, A15, GRFUNC_1:8
.= I . l by A9, A15, GRFUNC_1:8 ;
hence IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,(k + 1)))),(Comput ((ProgramPart s1),s1,(k + 1))))),n) = (Relocated (I,n)) . (l + n) by A16, COMPOS_1:122
.= (ProgramPart (Relocated (I,n))) . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by A19, FUNCT_1:72
.= s2 . (IC (Comput ((ProgramPart s2),s2,(k + 1)))) by A3, A20, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,(k + 1)))),(Comput ((ProgramPart s2),s2,(k + 1)))) by Z, AMI_1:54 ;
:: thesis: DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1)))
thus DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) by A11, A12, A18, A14, A17, SCMFSA6A:41, XXREAL_0:2; :: thesis: verum
end;
A21: S2[ 0 ]
proof
A22: IC (Comput ((ProgramPart (s1 +* (I +* (Start-At (0,SCM+FSA))))),(s1 +* (I +* (Start-At (0,SCM+FSA)))),0)) = IC (s1 +* (I +* (Start-At (0,SCM+FSA)))) by EXTPRO_1:3
.= IC ((s1 +* I) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= 0 by FUNCT_4:121 ;
assume 0 < pseudo-LifeSpan (s1,I) ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,0))) + n = IC (Comput ((ProgramPart s2),s2,0)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,0))),(Comput ((ProgramPart s1),s1,0)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,0))),(Comput ((ProgramPart s2),s2,0))) & DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart (Comput ((ProgramPart s2),s2,0)) )
then A23: 0 in dom I by A2, A22, SCMFSA8A:def 5;
then A24: 0 in dom (ProgramPart I) by RELAT_1:209;
A25: IC SCM+FSA in dom (I +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
u: Comput ((ProgramPart s1),s1,0) = s1 by EXTPRO_1:3;
v: Comput ((ProgramPart s2),s2,0) = s2 by EXTPRO_1:3;
IC (Comput ((ProgramPart s1),s1,0)) = s1 . (IC SCM+FSA) by EXTPRO_1:3
.= IC (I +* (Start-At (0,SCM+FSA))) by A1, A25, GRFUNC_1:8
.= 0 by COMPOS_1:142 ;
hence (IC (Comput ((ProgramPart s1),s1,0))) + n = IC (Comput ((ProgramPart s2),s2,0)) by A4, EXTPRO_1:3; :: thesis: ( IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,0))),(Comput ((ProgramPart s1),s1,0)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,0))),(Comput ((ProgramPart s2),s2,0))) & DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart (Comput ((ProgramPart s2),s2,0)) )
A26: I c= I +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A27: dom I c= dom (I +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
0 + n in dom (Relocated (I,n)) by A23, COMPOS_1:118;
then A28: 0 + n in dom (ProgramPart (Relocated (I,n))) by COMPOS_1:16;
IC SCM+FSA in dom (I +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
then A29: s1 . (IC s1) = s1 . (IC (I +* (Start-At (0,SCM+FSA)))) by A1, GRFUNC_1:8
.= s1 . 0 by COMPOS_1:142
.= (I +* (Start-At (0,SCM+FSA))) . 0 by A1, A27, A23, GRFUNC_1:8
.= I . 0 by A26, A23, GRFUNC_1:8 ;
Y: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
Z: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
thus IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,0))),(Comput ((ProgramPart s1),s1,0)))),n) = IncAddr ((CurInstr ((ProgramPart s1),s1)),n) by u
.= (Relocated (I,n)) . (0 + n) by A29, A24, Y, COMPOS_1:122
.= (ProgramPart (Relocated (I,n))) . n by FUNCT_1:72
.= CurInstr ((ProgramPart s2),s2) by A3, A4, A28, Z, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,0))),(Comput ((ProgramPart s2),s2,0))) by v ; :: thesis: DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart (Comput ((ProgramPart s2),s2,0))
thus DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart s2 by A5, EXTPRO_1:3
.= DataPart (Comput ((ProgramPart s2),s2,0)) by EXTPRO_1:3 ; :: thesis: verum
end;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A21, A8);
hence IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),n) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(Comput ((ProgramPart s2),s2,i))) by A7; :: thesis: verum
end;
A30: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A31: S1[k] ; :: thesis: S1[k + 1]
set i = CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)));
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,k)) by AMI_1:123;
A32: Comput ((ProgramPart s2),s2,(k + 1)) = Following ((ProgramPart s2),(Comput ((ProgramPart s2),s2,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,k))),(Comput ((ProgramPart s2),s2,k)))),(Comput ((ProgramPart s2),s2,k))) by T ;
assume A33: k + 1 <= pseudo-LifeSpan (s1,I) ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,(k + 1)))) + n = IC (Comput ((ProgramPart s2),s2,(k + 1))) & DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1))) )
then A34: k + 1 <= (pseudo-LifeSpan (s1,I)) + 1 by NAT_1:12;
A35: k < pseudo-LifeSpan (s1,I) by A33, NAT_1:13;
T: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,k)) by AMI_1:123;
A36: Comput ((ProgramPart s1),s1,(k + 1)) = Following ((ProgramPart s1),(Comput ((ProgramPart s1),s1,k))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))),(Comput ((ProgramPart s1),s1,k))) by T ;
hence (IC (Comput ((ProgramPart s1),s1,(k + 1)))) + n = IC (Exec ((IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))),n)),(Comput ((ProgramPart s2),s2,k)))) by A31, A34, SCMFSA6A:41, XREAL_1:8
.= IC (Comput ((ProgramPart s2),s2,(k + 1))) by A6, A35, A32 ;
:: thesis: DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Comput ((ProgramPart s2),s2,(k + 1)))
thus DataPart (Comput ((ProgramPart s1),s1,(k + 1))) = DataPart (Exec ((IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,k))),(Comput ((ProgramPart s1),s1,k)))),n)),(Comput ((ProgramPart s2),s2,k)))) by A31, A34, A36, SCMFSA6A:41, XREAL_1:8
.= DataPart (Comput ((ProgramPart s2),s2,(k + 1))) by A6, A35, A32 ; :: thesis: verum
end;
let i be Element of NAT ; :: thesis: ( i <= pseudo-LifeSpan (s1,I) implies ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) )
assume A37: i <= pseudo-LifeSpan (s1,I) ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )
A38: S1[ 0 ]
proof
assume 0 <= pseudo-LifeSpan (s1,I) ; :: thesis: ( (IC (Comput ((ProgramPart s1),s1,0))) + n = IC (Comput ((ProgramPart s2),s2,0)) & DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart (Comput ((ProgramPart s2),s2,0)) )
A39: IC SCM+FSA in dom (I +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
IC (Comput ((ProgramPart s1),s1,0)) = s1 . (IC SCM+FSA) by EXTPRO_1:3
.= IC (I +* (Start-At (0,SCM+FSA))) by A1, A39, GRFUNC_1:8
.= 0 by COMPOS_1:142 ;
hence (IC (Comput ((ProgramPart s1),s1,0))) + n = IC (Comput ((ProgramPart s2),s2,0)) by A4, EXTPRO_1:3; :: thesis: DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart (Comput ((ProgramPart s2),s2,0))
thus DataPart (Comput ((ProgramPart s1),s1,0)) = DataPart s2 by A5, EXTPRO_1:3
.= DataPart (Comput ((ProgramPart s2),s2,0)) by EXTPRO_1:3 ; :: thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A38, A30);
 hence ( (IC (Comput ((ProgramPart s1),s1,i))) + n = IC (Comput ((ProgramPart s2),s2,i)) & DataPart (Comput ((ProgramPart s1),s1,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) ) by A37; :: thesis: verum