let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of
for k being Nat st I c= P & k < LifeSpan ((P +* (stop I)),s) holds
CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS
let s be 0 -started State of SCMPDS; for I being halt-free parahalting Program of
for k being Nat st I c= P & k < LifeSpan ((P +* (stop I)),s) holds
CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS
let I be halt-free parahalting Program of ; for k being Nat st I c= P & k < LifeSpan ((P +* (stop I)),s) holds
CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS
let k be Nat; ( I c= P & k < LifeSpan ((P +* (stop I)),s) implies CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS )
set PI = P +* (stop I);
set s1 = Comput (P,s,k);
set s2 = Comput ((P +* (stop I)),s,k);
assume that
A1:
I c= P
and
A2:
k < LifeSpan ((P +* (stop I)),s)
; CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS
A3:
IC (Comput ((P +* (stop I)),s,k)) in dom I
by A2, Th12;
A4:
P /. (IC (Comput (P,s,k))) = P . (IC (Comput (P,s,k)))
by PBOOLE:143;
CurInstr (P,(Comput (P,s,k))) =
P . (IC (Comput ((P +* (stop I)),s,k)))
by A4, A1, A2, Th13
.=
I . (IC (Comput ((P +* (stop I)),s,k)))
by A1, A3, GRFUNC_1:2
;
hence
CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS
by A3, COMPOS_1:def 27; verum