let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for s1 being 0 -started State of SCM+FSA
for s2 being State of SCM+FSA
for I being Program of SCM+FSA st I c= P1 & I is_pseudo-closed_on s1,P1 holds
for n being Element of NAT st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )
let s1 be 0 -started State of SCM+FSA; :: thesis: for s2 being State of SCM+FSA
for I being Program of SCM+FSA st I c= P1 & I is_pseudo-closed_on s1,P1 holds
for n being Element of NAT st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )
let s2 be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I c= P1 & I is_pseudo-closed_on s1,P1 holds
for n being Element of NAT st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )
let I be Program of SCM+FSA; :: thesis: ( I c= P1 & I is_pseudo-closed_on s1,P1 implies for n being Element of NAT st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) ) )
A1: Start-At (0,SCM+FSA) c= s1 by MEMSTR_0:29;
assume A2: I c= P1 ; :: thesis: ( not I is_pseudo-closed_on s1,P1 or for n being Element of NAT st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) ) )
then A3: P1 = P1 +* I by FUNCT_4:98;
assume A4: I is_pseudo-closed_on s1,P1 ; :: thesis: for n being Element of NAT st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )
let n be Element of NAT ; :: thesis: ( Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 implies ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) ) )
assume A6: Reloc (I,n) c= P2 ; :: thesis: ( not IC s2 = n or not DataPart s1 = DataPart s2 or ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) ) )
defpred S1[ Nat] means ( $1 <= pseudo-LifeSpan (s1,P1,I) implies ( (IC (Comput (P1,s1,$1))) + n = IC (Comput (P2,s2,$1)) & DataPart (Comput (P1,s1,$1)) = DataPart (Comput (P2,s2,$1)) ) );
assume A7: IC s2 = n ; :: thesis: ( not DataPart s1 = DataPart s2 or ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) ) )
assume A8: DataPart s1 = DataPart s2 ; :: thesis: ( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )
hereby :: thesis: for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
defpred S2[ Nat] means ( $1 < pseudo-LifeSpan (s1,P1,I) implies ( (IC (Comput (P1,s1,$1))) + n = IC (Comput (P2,s2,$1)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,$1)))),n) = CurInstr (P2,(Comput (P2,s2,$1))) & DataPart (Comput (P1,s1,$1)) = DataPart (Comput (P2,s2,$1)) ) );
let i be Element of NAT ; :: thesis: ( i < pseudo-LifeSpan (s1,P1,I) implies IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) )
assume A10: i < pseudo-LifeSpan (s1,P1,I) ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i)))
A11: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A12: S2[k] ; :: thesis: S2[k + 1]
reconsider l = IC (Comput (P1,s1,(k + 1))) as Element of NAT ;
reconsider j = CurInstr (P1,(Comput (P1,s1,(k + 1)))) as Instruction of SCM+FSA ;
assume A14: k + 1 < pseudo-LifeSpan (s1,P1,I) ; :: thesis: ( (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) & IncAddr ((CurInstr (P1,(Comput (P1,s1,(k + 1))))),n) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )
A15: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3;
B16: Initialize s1 = s1 by A1, FUNCT_4:98;
then A16: IC (Comput (P1,s1,(k + 1))) in dom I by A4, A14, A3, SCMFSA8A:def 4;
A17: l in dom I by B16, A4, A14, A3, SCMFSA8A:def 4;
A18: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3;
A19: k + 0 < k + 1 by XREAL_1:6;
hence A20: (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) by A12, A14, A15, A18, SCMFSA6A:8, XXREAL_0:2; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(k + 1))))),n) = CurInstr (P2,(Comput (P2,s2,(k + 1)))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )
then A21: IC (Comput (P2,s2,(k + 1))) in dom (Reloc (I,n)) by A16, COMPOS_1:46;
j = P1 . (IC (Comput (P1,s1,(k + 1)))) by PBOOLE:143
.= I . l by A16, A2, GRFUNC_1:2 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(k + 1))))),n) = (Reloc (I,n)) . (l + n) by A17, COMPOS_1:35
.= P2 . (IC (Comput (P2,s2,(k + 1)))) by A21, A20, A6, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(k + 1)))) by PBOOLE:143 ;
:: thesis: DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1)))
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) by A12, A14, A19, A15, A18, SCMFSA6A:8, XXREAL_0:2; :: thesis: verum
end;
A23: S2[ 0 ]
proof
X: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A24: IC (Comput ((P1 +* I),(Initialize s1),0)) = IC (Initialize s1) by EXTPRO_1:2
.= IC (Start-At (0,SCM+FSA)) by X, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
assume 0 < pseudo-LifeSpan (s1,P1,I) ; :: thesis: ( (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),n) = CurInstr (P2,(Comput (P2,s2,0))) & DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) )
then A25: 0 in dom I by A4, A24, SCMFSA8A:def 4;
A27: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A28: Comput (P1,s1,0) = s1 by EXTPRO_1:2;
A29: Comput (P2,s2,0) = s2 by EXTPRO_1:2;
IC (Comput (P1,s1,0)) = s1 . (IC ) by EXTPRO_1:2
.= IC (Start-At (0,SCM+FSA)) by A1, A27, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
hence (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) by A7, EXTPRO_1:2; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),n) = CurInstr (P2,(Comput (P2,s2,0))) & DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) )
A30: 0 + n in dom (Reloc (I,n)) by A25, COMPOS_1:46;
A32: P1 . (IC s1) = P1 . (IC (Start-At (0,SCM+FSA))) by A1, A27, GRFUNC_1:2
.= P1 . 0 by FUNCOP_1:72
.= I . 0 by A25, A2, GRFUNC_1:2 ;
A33: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A34: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),n) = (Reloc (I,n)) . (0 + n) by A25, A33, A28, A32, COMPOS_1:35
.= CurInstr (P2,(Comput (P2,s2,0))) by A29, A7, A30, A34, A6, GRFUNC_1:2 ; :: thesis: DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0))
thus DataPart (Comput (P1,s1,0)) = DataPart s2 by A8, EXTPRO_1:2
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:2 ; :: thesis: verum
end;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A23, A11);
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) by A10; :: thesis: verum
end;
A35: 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 A36: S1[k] ; :: thesis: S1[k + 1]
set i = CurInstr (P1,(Comput (P1,s1,k)));
A37: Comput (P2,s2,(k + 1)) = Following (P2,(Comput (P2,s2,k))) by EXTPRO_1:3;
assume A38: k + 1 <= pseudo-LifeSpan (s1,P1,I) ; :: thesis: ( (IC (Comput (P1,s1,(k + 1)))) + n = IC (Comput (P2,s2,(k + 1))) & DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1))) )
then A39: k + 1 <= (pseudo-LifeSpan (s1,P1,I)) + 1 by NAT_1:12;
A40: k < pseudo-LifeSpan (s1,P1,I) by A38, NAT_1:13;
A41: Comput (P1,s1,(k + 1)) = Following (P1,(Comput (P1,s1,k))) by EXTPRO_1:3;
hence (IC (Comput (P1,s1,(k + 1)))) + n = IC (Exec ((IncAddr ((CurInstr (P1,(Comput (P1,s1,k)))),n)),(Comput (P2,s2,k)))) by A36, A39, SCMFSA6A:8, XREAL_1:6
.= IC (Comput (P2,s2,(k + 1))) by A9, A40, A37 ;
:: thesis: DataPart (Comput (P1,s1,(k + 1))) = DataPart (Comput (P2,s2,(k + 1)))
thus DataPart (Comput (P1,s1,(k + 1))) = DataPart (Exec ((IncAddr ((CurInstr (P1,(Comput (P1,s1,k)))),n)),(Comput (P2,s2,k)))) by A36, A39, A41, SCMFSA6A:8, XREAL_1:6
.= DataPart (Comput (P2,s2,(k + 1))) by A9, A40, A37 ; :: thesis: verum
end;
let i be Element of NAT ; :: thesis: ( i <= pseudo-LifeSpan (s1,P1,I) implies ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) )
assume A42: i <= pseudo-LifeSpan (s1,P1,I) ; :: thesis: ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
A43: S1[ 0 ]
proof
assume 0 <= pseudo-LifeSpan (s1,P1,I) ; :: thesis: ( (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) & DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0)) )
A44: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
IC (Comput (P1,s1,0)) = s1 . (IC ) by EXTPRO_1:2
.= IC (Start-At (0,SCM+FSA)) by A1, A44, GRFUNC_1:2
.= 0 by FUNCOP_1:72 ;
hence (IC (Comput (P1,s1,0))) + n = IC (Comput (P2,s2,0)) by A7, EXTPRO_1:2; :: thesis: DataPart (Comput (P1,s1,0)) = DataPart (Comput (P2,s2,0))
thus DataPart (Comput (P1,s1,0)) = DataPart s2 by A8, EXTPRO_1:2
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:2 ; :: thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A43, A35);
 hence ( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) by A42; :: thesis: verum