let P1, P2 be Instruction-Sequence of SCM+FSA; for s1, s2 being State of SCM+FSA
for I being really-closed Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_halting_on s1,P1 holds
I is_halting_on s2,P2
let s1, s2 be State of SCM+FSA; for I being really-closed Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_halting_on s1,P1 holds
I is_halting_on s2,P2
let I be really-closed Program of SCM+FSA; ( DataPart s1 = DataPart s2 & I is_halting_on s1,P1 implies I is_halting_on s2,P2 )
set S1 = Initialize s1;
set S2 = Initialize s2;
IC (Initialize s1) = 0
by MEMSTR_0:47;
then A1:
IC (Initialize s1) in dom I
by AFINSQ_1:65;
A2:
I c= P1 +* I
by FUNCT_4:25;
defpred S1[ Nat] means ( IC (Comput ((P1 +* I),(Initialize s1),$1)) = IC (Comput ((P2 +* I),(Initialize s2),$1)) & CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),$1))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),$1))) & DataPart (Comput ((P1 +* I),(Initialize s1),$1)) = DataPart (Comput ((P2 +* I),(Initialize s2),$1)) );
A3:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
A4: IC (Comput ((P1 +* I),(Initialize s1),0)) =
IC (Start-At (0,SCM+FSA))
by A3, FUNCT_4:13
.=
0
by FUNCOP_1:72
;
A5: IC (Comput ((P2 +* I),(Initialize s2),0)) =
IC (Start-At (0,SCM+FSA))
by A3, FUNCT_4:13
.=
0
by FUNCOP_1:72
;
assume
DataPart s1 = DataPart s2
; ( not I is_halting_on s1,P1 or I is_halting_on s2,P2 )
then A6:
Comput ((P1 +* I),(Initialize s1),0) = Comput ((P2 +* I),(Initialize s2),0)
by MEMSTR_0:80;
A7:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )A8:
Comput (
(P2 +* I),
(Initialize s2),
(k + 1)) =
Following (
(P2 +* I),
(Comput ((P2 +* I),(Initialize s2),k)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),k)))),
(Comput ((P2 +* I),(Initialize s2),k)))
;
assume A9:
S1[
k]
;
S1[k + 1]then A10:
for
f being
FinSeq-Location holds
(Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f
by SCMFSA_M:2;
for
a being
Int-Location holds
(Comput ((P1 +* I),(Initialize s1),k)) . a = (Comput ((P2 +* I),(Initialize s2),k)) . a
by A9, SCMFSA_M:2;
then A11:
Comput (
(P1 +* I),
(Initialize s1),
k)
= Comput (
(P2 +* I),
(Initialize s2),
k)
by A9, A10, SCMFSA_2:61;
A12:
IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) in dom I
by A1, A2, AMISTD_1:21;
Comput (
(P1 +* I),
(Initialize s1),
(k + 1)) =
Following (
(P1 +* I),
(Comput ((P1 +* I),(Initialize s1),k)))
by EXTPRO_1:3
.=
Exec (
(CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),k)))),
(Comput ((P1 +* I),(Initialize s1),k)))
;
then A13:
Comput (
(P1 +* I),
(Initialize s1),
(k + 1))
= Comput (
(P2 +* I),
(Initialize s2),
(k + 1))
by A9, A11, A8;
A14:
IC (Comput ((P1 +* I),(Initialize s1),(k + 1))) = IC (Comput ((P2 +* I),(Initialize s2),(k + 1)))
by A13;
A15:
(P1 +* I) /. (IC (Comput ((P1 +* I),(Initialize s1),(k + 1)))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),(k + 1))))
by PBOOLE:143;
A16:
(P2 +* I) /. (IC (Comput ((P2 +* I),(Initialize s2),(k + 1)))) = (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),(k + 1))))
by PBOOLE:143;
A17:
I c= P1 +* I
by FUNCT_4:25;
A18:
I c= P2 +* I
by FUNCT_4:25;
CurInstr (
(P1 +* I),
(Comput ((P1 +* I),(Initialize s1),(k + 1)))) =
I . (IC (Comput ((P1 +* I),(Initialize s1),(k + 1))))
by A12, A15, A17, GRFUNC_1:2
.=
CurInstr (
(P2 +* I),
(Comput ((P2 +* I),(Initialize s2),(k + 1))))
by A14, A12, A16, A18, GRFUNC_1:2
;
hence
S1[
k + 1]
by A13;
verum end;
assume
I is_halting_on s1,P1
; I is_halting_on s2,P2
then
P1 +* I halts_on Initialize s1
by SCMFSA7B:def 7;
then consider m being Nat such that
A19:
CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),m))) = halt SCM+FSA
;
A20:
(P1 +* I) /. (IC (Comput ((P1 +* I),(Initialize s1),0))) = (P1 +* I) . (IC (Comput ((P1 +* I),(Initialize s1),0)))
by PBOOLE:143;
A21:
(P2 +* I) /. (IC (Comput ((P2 +* I),(Initialize s2),0))) = (P2 +* I) . (IC (Comput ((P2 +* I),(Initialize s2),0)))
by PBOOLE:143;
A22:
0 in dom I
by AFINSQ_1:65;
then CurInstr ((P1 +* I),(Comput ((P1 +* I),(Initialize s1),0))) =
I . 0
by A4, A20, FUNCT_4:13
.=
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),0)))
by A5, A22, A21, FUNCT_4:13
;
then A23:
S1[ 0 ]
by A6;
for k being Nat holds S1[k]
from NAT_1:sch 2(A23, A7);
then
CurInstr ((P2 +* I),(Comput ((P2 +* I),(Initialize s2),m))) = halt SCM+FSA
by A19;
then
P2 +* I halts_on Initialize s2
by EXTPRO_1:29;
hence
I is_halting_on s2,P2
by SCMFSA7B:def 7; verum