let P1, P2 be Instruction-Sequence of SCM+FSA; for s being 0 -started State of SCM+FSA
for I being really-closed parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
let s be 0 -started State of SCM+FSA; for I being really-closed parahalting Program of st I c= P1 & I c= P2 holds
( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
let I be really-closed parahalting Program of ; ( I c= P1 & I c= P2 implies ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) )
assume that
A1:
I c= P1
and
A2:
I c= P2
; ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )
A3:
P2 halts_on s
by A2, AMISTD_1:def 11;
A4:
P1 halts_on s
by A1, AMISTD_1:def 11;
A5:
now for l being Nat st CurInstr (P2,(Comput (P2,s,l))) = halt SCM+FSA holds
LifeSpan (P1,s) <= llet l be
Nat;
( CurInstr (P2,(Comput (P2,s,l))) = halt SCM+FSA implies LifeSpan (P1,s) <= l )assume A6:
CurInstr (
P2,
(Comput (P2,s,l)))
= halt SCM+FSA
;
LifeSpan (P1,s) <= l
CurInstr (
P1,
(Comput (P1,s,l)))
= CurInstr (
P2,
(Comput (P2,s,l)))
by Th7, A1, A2;
hence
LifeSpan (
P1,
s)
<= l
by A4, A6, EXTPRO_1:def 15;
verum end;
CurInstr (P2,(Comput (P2,s,(LifeSpan (P1,s))))) =
CurInstr (P1,(Comput (P1,s,(LifeSpan (P1,s)))))
by Th7, A1, A2
.=
halt SCM+FSA
by A4, EXTPRO_1:def 15
;
hence A7:
LifeSpan (P1,s) = LifeSpan (P2,s)
by A5, A3, EXTPRO_1:def 15; Result (P1,s) = Result (P2,s)
A8:
Result (P2,s) = Comput (P2,s,(LifeSpan (P1,s)))
by A7, Th1, A2, EXTPRO_1:23;
Result (P1,s) = Comput (P1,s,(LifeSpan (P1,s)))
by Th1, A1, EXTPRO_1:23;
hence
Result (P1,s) = Result (P2,s)
by A8, Th7, A1, A2; verum