let s be State of ; :: thesis: for I being parahalting No-StopCode Program of
for k being Element of NAT st Initialized I c= s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation s,k) <> halt SCMPDS
let I be parahalting No-StopCode Program of ; :: thesis: for k being Element of NAT st Initialized I c= s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation s,k) <> halt SCMPDS
let k be Element of NAT ; :: thesis: ( Initialized I c= s & k < LifeSpan (s +* (Initialized (stop I))) implies CurInstr (Computation s,k) <> halt SCMPDS )
set sI = s +* (Initialized (stop I));
set s1 = Computation s,k;
set s2 = Computation (s +* (Initialized (stop I))),k;
assume that
A1: Initialized I c= s and
A2: k < LifeSpan (s +* (Initialized (stop I))) ; :: thesis: CurInstr (Computation s,k) <> halt SCMPDS
A3: I c= Computation s,k by A1, AMI_1:81, SCMPDS_4:57;
A4: IC (Computation (s +* (Initialized (stop I))),k) in dom I by A2, Th28;
CurInstr (Computation s,k) = (Computation s,k) . (IC (Computation (s +* (Initialized (stop I))),k)) by A1, A2, Th29, AMI_1:121
.= I . (IC (Computation (s +* (Initialized (stop I))),k)) by A3, A4, GRFUNC_1:8 ;
hence CurInstr (Computation s,k) <> halt SCMPDS by A4, Def3; :: thesis: verum