let s1, s2 be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I +* (Start-At (insloc 0 )) c= s1 & I is_closed_on s1 holds
for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
let I be Program of SCM+FSA ; :: thesis: ( I +* (Start-At (insloc 0 )) c= s1 & I is_closed_on s1 implies for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
assume A1:
I +* (Start-At (insloc 0 )) c= s1
; :: thesis: ( not I is_closed_on s1 or for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
assume A2:
I is_closed_on s1
; :: thesis: for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
let n be Element of NAT ; :: thesis: ( ProgramPart (Relocated I,n) c= s2 & IC s2 = insloc n & DataPart s1 = DataPart s2 implies for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
assume A3:
ProgramPart (Relocated I,n) c= s2
; :: thesis: ( not IC s2 = insloc n or not DataPart s1 = DataPart s2 or for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
assume A4:
IC s2 = insloc n
; :: thesis: ( not DataPart s1 = DataPart s2 or for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
assume A5:
DataPart s1 = DataPart s2
; :: thesis: for i being Element of NAT holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
let i be Element of NAT ; :: thesis: ( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
defpred S1[ Element of NAT ] means ( (IC (Computation s1,$1)) + n = IC (Computation s2,$1) & IncAddr (CurInstr (Computation s1,$1)),n = CurInstr (Computation s2,$1) & DataPart (Computation s1,$1) = DataPart (Computation s2,$1) );
A6:
S1[ 0 ]
proof
A7:
IC SCM+FSA in dom (I +* (Start-At (insloc 0 )))
by SF_MASTR:65;
IC (Computation s1,0 ) =
s1 . (IC SCM+FSA )
by AMI_1:13
.=
(I +* (Start-At (insloc 0 ))) . (IC SCM+FSA )
by A1, A7, GRFUNC_1:8
.=
insloc 0
by SF_MASTR:66
;
hence
(IC (Computation s1,0 )) + n = IC (Computation s2,0 )
by A4, AMI_1:13;
:: thesis: ( IncAddr (CurInstr (Computation s1,0 )),n = CurInstr (Computation s2,0 ) & DataPart (Computation s1,0 ) = DataPart (Computation s2,0 ) )
A8:
I c= I +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
then A9:
dom I c= dom (I +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
A10:
insloc 0 in dom I
by A2, Th3;
IC SCM+FSA in dom (I +* (Start-At (insloc 0 )))
by SF_MASTR:65;
then A11:
s1 . (IC s1) =
s1 . ((I +* (Start-At (insloc 0 ))) . (IC SCM+FSA ))
by A1, GRFUNC_1:8
.=
s1 . (insloc 0 )
by SF_MASTR:66
.=
(I +* (Start-At (insloc 0 ))) . (insloc 0 )
by A1, A9, A10, GRFUNC_1:8
.=
I . (insloc 0 )
by A8, A10, GRFUNC_1:8
;
(insloc 0 ) + n in dom (Relocated I,n)
by A10, SCMFSA_5:4;
then A12:
insloc (0 + n) in dom (ProgramPart (Relocated I,n))
by AMI_1:106;
ProgramPart I = I
by AMI_1:105;
then A13:
insloc 0 in dom (ProgramPart I)
by A2, Th3;
thus IncAddr (CurInstr (Computation s1,0 )),
n =
IncAddr (CurInstr s1),
n
by AMI_1:13
.=
(Relocated I,n) . ((insloc 0 ) + n)
by A11, A13, SCMFSA_5:7
.=
(ProgramPart (Relocated I,n)) . (insloc n)
by FUNCT_1:72
.=
CurInstr s2
by A3, A4, A12, GRFUNC_1:8
.=
CurInstr (Computation s2,0 )
by AMI_1:13
;
:: thesis: DataPart (Computation s1,0 ) = DataPart (Computation s2,0 )
thus DataPart (Computation s1,0 ) =
DataPart s2
by A5, AMI_1:13
.=
DataPart (Computation s2,0 )
by AMI_1:13
;
:: thesis: verum
end;
A15:
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 A16:
S1[
k]
;
:: thesis: S1[k + 1]
A17:
Computation s1,
(k + 1) =
Following (Computation s1,k)
by AMI_1:14
.=
Exec (CurInstr (Computation s1,k)),
(Computation s1,k)
;
A18:
Computation s2,
(k + 1) =
Following (Computation s2,k)
by AMI_1:14
.=
Exec (CurInstr (Computation s2,k)),
(Computation s2,k)
;
hence A19:
(IC (Computation s1,(k + 1))) + n = IC (Computation s2,(k + 1))
by A16, A17, SCMFSA6A:41;
:: thesis: ( IncAddr (CurInstr (Computation s1,(k + 1))),n = CurInstr (Computation s2,(k + 1)) & DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) )
reconsider j =
CurInstr (Computation s1,(k + 1)) as
Instruction of
SCM+FSA ;
reconsider l =
IC (Computation s1,(k + 1)) as
Element of
NAT by ORDINAL1:def 13;
A20:
I c= I +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
then A21:
dom I c= dom (I +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
s1 +* (I +* (Start-At (insloc 0 ))) = s1
by A1, FUNCT_4:79;
then A22:
IC (Computation s1,(k + 1)) in dom I
by A2, SCMFSA7B:def 7;
A24:
IC (Computation s2,(k + 1)) in NAT
by AMI_1:def 4;
dom (ProgramPart I) = (dom I) /\ NAT
by RELAT_1:90;
then A25:
l in dom (ProgramPart I)
by A22, XBOOLE_0:def 4;
A26:
j =
s1 . (IC (Computation s1,(k + 1)))
by AMI_1:54
.=
(I +* (Start-At (insloc 0 ))) . (IC (Computation s1,(k + 1)))
by A1, A21, A22, GRFUNC_1:8
.=
I . l
by A20, A22, GRFUNC_1:8
;
IC (Computation s2,(k + 1)) in dom (Relocated I,n)
by A19, A22, SCMFSA_5:4;
then
IC (Computation s2,(k + 1)) in (dom (Relocated I,n)) /\ NAT
by A24, XBOOLE_0:def 4;
then A27:
IC (Computation s2,(k + 1)) in dom (ProgramPart (Relocated I,n))
by RELAT_1:90;
thus IncAddr (CurInstr (Computation s1,(k + 1))),
n =
(Relocated I,n) . (l + n)
by A25, A26, SCMFSA_5:7
.=
(ProgramPart (Relocated I,n)) . (IC (Computation s2,(k + 1)))
by A19, FUNCT_1:72
.=
s2 . (IC (Computation s2,(k + 1)))
by A3, A27, GRFUNC_1:8
.=
CurInstr (Computation s2,(k + 1))
by AMI_1:54
;
:: thesis: DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1))
thus
DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1))
by A16, A17, A18, SCMFSA6A:41;
:: thesis: verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A6, A15);
hence
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & IncAddr (CurInstr (Computation s1,i)),n = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
; :: thesis: verum