let P1, P2 be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
let s be 0 -started State of SCMPDS; for I being Program of st I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
let I be Program of ; ( I is_closed_on s,P1 & I is_halting_on s,P1 & stop I c= P1 & stop I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )
assume that
A1:
I is_closed_on s,P1
and
A2:
I is_halting_on s,P1
and
A3:
stop I c= P1
and
A4:
stop I c= P2
; ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
A5:
Start-At (0,SCMPDS) c= s
by MEMSTR_0:29;
A6:
Start-At (0,SCMPDS) c= s
by MEMSTR_0:29;
DataPart s = DataPart s
;
then A7:
I is_halting_on s,P2
by A1, A2, SCMPDS_6:23;
A8:
Initialize s = s
by A5, FUNCT_4:98;
A9:
Initialize s = s
by A6, FUNCT_4:98;
P2 = P2 +* (stop I)
by A4, FUNCT_4:98;
then A10:
P2 halts_on s
by A7, A9, SCMPDS_6:def 3;
P1 = P1 +* (stop I)
by A3, FUNCT_4:98;
then A11:
P1 halts_on s
by A2, A8, SCMPDS_6:def 3;
A12:
now for l being Nat st CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS holds
LifeSpan (P1,s) <= llet l be
Nat;
( CurInstr (P2,(Comput (P2,s,l))) = halt SCMPDS implies LifeSpan (P1,s) <= l )assume A13:
CurInstr (
P2,
(Comput (P2,s,l)))
= halt SCMPDS
;
LifeSpan (P1,s) <= l
CurInstr (
P1,
(Comput (P1,s,l)))
= CurInstr (
P2,
(Comput (P2,s,l)))
by A1, A3, A4, Th7;
hence
LifeSpan (
P1,
s)
<= l
by A11, A13, EXTPRO_1:def 15;
verum end;
CurInstr (P2,(Comput (P2,s,(LifeSpan (P1,s))))) =
CurInstr (P1,(Comput (P1,s,(LifeSpan (P1,s)))))
by A1, A3, A4, Th7
.=
halt SCMPDS
by A11, EXTPRO_1:def 15
;
hence
LifeSpan (P1,s) = LifeSpan (P2,s)
by A12, A10, EXTPRO_1:def 15; Result (P1,s) = Result (P2,s)
then A14:
Result (P2,s) = Comput (P2,s,(LifeSpan (P1,s)))
by A10, EXTPRO_1:23;
Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s)))
by A11, EXTPRO_1:23;
hence
Result (P1,s) = Result (P2,s)
by A1, A3, A4, A14, Th7; verum