let s2 be State of SCM+FSA; for s1 being 0 -started State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA
for J being really-closed parahalting Program of st J c= P holds
for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let s1 be 0 -started State of SCM+FSA; for P, Q being Instruction-Sequence of SCM+FSA
for J being really-closed parahalting Program of st J c= P holds
for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let P, Q be Instruction-Sequence of SCM+FSA; for J being really-closed parahalting Program of st J c= P holds
for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
let J be really-closed parahalting Program of ; ( J c= P implies for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) ) )
A1:
Start-At (0,SCM+FSA) c= s1
by MEMSTR_0:29;
assume A2:
J c= P
; for n being Nat st Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
set JAt = Start-At (0,SCM+FSA);
A3:
0 in dom J
by AFINSQ_1:65;
A4:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
then A5: P . (IC s1) =
P . (IC (Start-At (0,SCM+FSA)))
by A1, GRFUNC_1:2
.=
P . 0
by FUNCOP_1:72
.=
J . 0
by A3, A2, GRFUNC_1:2
;
A6: IC (Comput (P,s1,0)) =
IC s1
.=
IC (Start-At (0,SCM+FSA))
by A1, A4, GRFUNC_1:2
.=
0
by FUNCOP_1:72
;
A7:
0 in dom J
by AFINSQ_1:65;
let n be Nat; ( Reloc (J,n) c= Q & IC s2 = n & DataPart s1 = DataPart s2 implies for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) ) )
assume that
A8:
Reloc (J,n) c= Q
and
A9:
IC s2 = n
and
A10:
DataPart s1 = DataPart s2
; for i being Nat holds
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
A11: DataPart (Comput (P,s1,0)) =
DataPart s2
by A10
.=
DataPart (Comput (Q,s2,0))
;
defpred S1[ Nat] means ( (IC (Comput (P,s1,$1))) + n = IC (Comput (Q,s2,$1)) & IncAddr ((CurInstr (P,(Comput (P,s1,$1)))),n) = CurInstr (Q,(Comput (Q,s2,$1))) & DataPart (Comput (P,s1,$1)) = DataPart (Comput (Q,s2,$1)) );
A12:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
A13:
Comput (
P,
s1,
(k + 1)) =
Following (
P,
(Comput (P,s1,k)))
by EXTPRO_1:3
.=
Exec (
(CurInstr (P,(Comput (P,s1,k)))),
(Comput (P,s1,k)))
;
reconsider l =
IC (Comput (P,s1,(k + 1))) as
Element of
NAT ;
reconsider j =
CurInstr (
P,
(Comput (P,s1,(k + 1)))) as
Instruction of
SCM+FSA ;
A14:
Comput (
Q,
s2,
(k + 1)) =
Following (
Q,
(Comput (Q,s2,k)))
by EXTPRO_1:3
.=
Exec (
(CurInstr (Q,(Comput (Q,s2,k)))),
(Comput (Q,s2,k)))
;
IC s1 = 0
by MEMSTR_0:def 11;
then
IC s1 in dom J
by AFINSQ_1:65;
then A15:
IC (Comput (P,s1,(k + 1))) in dom J
by A2, AMISTD_1:21;
assume A16:
S1[
k]
;
S1[k + 1]
hence
(IC (Comput (P,s1,(k + 1)))) + n = IC (Comput (Q,s2,(k + 1)))
by A13, A14, SCMFSA6A:8;
( IncAddr ((CurInstr (P,(Comput (P,s1,(k + 1))))),n) = CurInstr (Q,(Comput (Q,s2,(k + 1)))) & DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1))) )
then A17:
IC (Comput (Q,s2,(k + 1))) in dom (Reloc (J,n))
by A15, COMPOS_1:46;
A18:
l in dom J
by A15;
A19:
dom P = NAT
by PARTFUN1:def 2;
A20:
dom Q = NAT
by PARTFUN1:def 2;
j =
P . (IC (Comput (P,s1,(k + 1))))
by A19, PARTFUN1:def 6
.=
J . l
by A15, A2, GRFUNC_1:2
;
hence IncAddr (
(CurInstr (P,(Comput (P,s1,(k + 1))))),
n) =
(Reloc (J,n)) . (l + n)
by A18, COMPOS_1:35
.=
(Reloc (J,n)) . (IC (Comput (Q,s2,(k + 1))))
by A16, A13, A14, SCMFSA6A:8
.=
Q . (IC (Comput (Q,s2,(k + 1))))
by A17, A8, GRFUNC_1:2
.=
CurInstr (
Q,
(Comput (Q,s2,(k + 1))))
by A20, PARTFUN1:def 6
;
DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1)))
thus
DataPart (Comput (P,s1,(k + 1))) = DataPart (Comput (Q,s2,(k + 1)))
by A16, A13, A14, SCMFSA6A:8;
verum
end;
let i be Nat; ( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
0 in dom J
by AFINSQ_1:65;
then A21:
0 + n in dom (Reloc (J,n))
by COMPOS_1:46;
A22:
dom Q = NAT
by PARTFUN1:def 2;
dom P = NAT
by PARTFUN1:def 2;
then IncAddr ((CurInstr (P,(Comput (P,s1,0)))),n) =
(Reloc (J,n)) . (0 + n)
by A5, A7, COMPOS_1:35, PARTFUN1:def 6
.=
Q . (IC (Comput (Q,s2,0)))
by A9, A21, A8, GRFUNC_1:2
.=
CurInstr (Q,(Comput (Q,s2,0)))
by A22, PARTFUN1:def 6
;
then A23:
S1[ 0 ]
by A9, A6, A11;
for k being Nat holds S1[k]
from NAT_1:sch 2(A23, A12);
hence
( (IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) & IncAddr ((CurInstr (P,(Comput (P,s1,i)))),n) = CurInstr (Q,(Comput (Q,s2,i))) & DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
; verum