let s1, s2 be State of SCM+FSA; for p1, p2 being Instruction-Sequence of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds
( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )
let p1, p2 be Instruction-Sequence of SCM+FSA; for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds
( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )
let I be really-closed InitHalting Program of SCM+FSA; ( Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 implies ( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) ) )
assume that
A1:
Initialize ((intloc 0) .--> 1) c= s1
and
A2:
Initialize ((intloc 0) .--> 1) c= s2
and
A3:
I c= p1
and
A4:
I c= p2
and
A5:
s1 = s2
; ( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )
A6:
p2 halts_on s2
by A2, Def1, A4;
A7:
p1 halts_on s1
by A1, Def1, A3;
A8:
now for l being Nat st CurInstr (p2,(Comput (p2,s2,l))) = halt SCM+FSA holds
LifeSpan (p1,s1) <= llet l be
Nat;
( CurInstr (p2,(Comput (p2,s2,l))) = halt SCM+FSA implies LifeSpan (p1,s1) <= l )assume A9:
CurInstr (
p2,
(Comput (p2,s2,l)))
= halt SCM+FSA
;
LifeSpan (p1,s1) <= l
CurInstr (
p1,
(Comput (p1,s1,l)))
= CurInstr (
p2,
(Comput (p2,s2,l)))
by A1, A5, Th5, A3, A4;
hence
LifeSpan (
p1,
s1)
<= l
by A7, A9, EXTPRO_1:def 15;
verum end;
CurInstr (p2,(Comput (p2,s2,(LifeSpan (p1,s1))))) =
CurInstr (p1,(Comput (p1,s1,(LifeSpan (p1,s1)))))
by A1, A5, Th5, A3, A4
.=
halt SCM+FSA
by A7, EXTPRO_1:def 15
;
hence A10:
LifeSpan (p1,s1) = LifeSpan (p2,s2)
by A8, A6, EXTPRO_1:def 15; Result (p1,s1) = Result (p2,s2)
p2 halts_on s2
by A2, Def1, A4;
then A11:
Result (p2,s2) = Comput (p2,s2,(LifeSpan (p1,s1)))
by A10, EXTPRO_1:23;
p1 halts_on s1
by A1, Def1, A3;
then
Result (p1,s1) = Comput (p1,s1,(LifeSpan (p1,s1)))
by EXTPRO_1:23;
hence
Result (p1,s1) = Result (p2,s2)
by A1, A5, A11, Th5, A3, A4; verum