let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for k being Element of 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; :: thesis: for I being halt-free parahalting Program of SCMPDS
for k being Element of 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 SCMPDS; :: thesis: for k being Element of NAT st I c= P & k < LifeSpan ((P +* (stop I)),s) holds
CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS
let k be Element of NAT ; :: thesis: ( 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) ; :: thesis: CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS
A4: IC (Comput ((P +* (stop I)),s,k)) in dom I by A2, Th28;
A6: 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 A6, A1, A2, Th29
.= I . (IC (Comput ((P +* (stop I)),s,k))) by A1, A4, GRFUNC_1:2 ;
hence CurInstr (P,(Comput (P,s,k))) <> halt SCMPDS by A4, COMPOS_1:def 25; :: thesis: verum