let P1, P2 be Instruction-Sequence of SCM+FSA; for s1, s2 being 0 -started State of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds
Result (P1,s1) = Result (P2,s2)
let s1, s2 be 0 -started State of SCM+FSA; for I being really-closed Program of SCM+FSA st I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 holds
Result (P1,s1) = Result (P2,s2)
set D = Data-Locations ;
let I be really-closed Program of SCM+FSA; ( I is_halting_on s1,P1 & I c= P1 & I c= P2 & ex k being Nat st Comput (P1,s1,k) = s2 implies Result (P1,s1) = Result (P2,s2) )
assume A1:
I is_halting_on s1,P1
; ( not I c= P1 or not I c= P2 or for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )
A2:
Start-At (0,SCM+FSA) c= s1
by MEMSTR_0:29;
A3:
s2 = Initialize s2
by MEMSTR_0:44;
assume
I c= P1
; ( not I c= P2 or for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )
then A4:
P1 = P1 +* I
by FUNCT_4:98;
assume
I c= P2
; ( for k being Nat holds not Comput (P1,s1,k) = s2 or Result (P1,s1) = Result (P2,s2) )
then A5:
P2 = P2 +* I
by FUNCT_4:98;
s1 = Initialize s1
by A2, FUNCT_4:98;
then A6:
P1 halts_on s1
by A1, A4;
then consider n being Nat such that
A7:
CurInstr (P1,(Comput (P1,s1,n))) = halt SCM+FSA
;
given k being Nat such that A8:
Comput (P1,s1,k) = s2
; Result (P1,s1) = Result (P2,s2)
set s3 = Comput (P1,s1,k);
set P3 = P1;
A9:
IC in dom (Comput (P1,s1,k))
by MEMSTR_0:2;
IC (Comput (P1,s1,k)) =
IC s2
by A8
.=
IC (Initialize s2)
by A3
.=
0
by FUNCT_4:113
;
then
(IC ) .--> 0 c= Comput (P1,s1,k)
by A9, FUNCOP_1:73;
then
Start-At (0,SCM+FSA) c= Comput (P1,s1,k)
;
then A10:
Comput (P1,s1,k) = Initialize (Comput (P1,s1,k))
by FUNCT_4:98;
A11:
Comput (P1,s1,(n + k)) = Comput (P1,(Comput (P1,s1,k)),n)
by EXTPRO_1:4;
A12:
Comput (P1,s1,(n + k)) = Comput (P1,s1,n)
by A7, EXTPRO_1:5, NAT_1:11;
P1 halts_on Comput (P1,s1,k)
by A7, A12, A11, EXTPRO_1:29;
then A13:
I is_halting_on Comput (P1,s1,k),P1
by A10, A4;
A14:
DataPart (Comput (P1,s1,k)) = DataPart s2
by A8;
consider k being Nat such that
A15:
CurInstr (P1,(Comput (P1,s1,k))) = halt SCM+FSA
by A6;
A16:
P1 . (IC (Comput (P1,s1,k))) = halt SCM+FSA
by A15, PBOOLE:143;
Result (P1,(Comput (P1,s1,k))) = Result (P2,s2)
by A3, A14, A10, A13, Th63, A4, A5;
hence
Result (P1,s1) = Result (P2,s2)
by A16, EXTPRO_1:8; verum