let P be Instruction-Sequence of SCMPDS; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: 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

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; :: thesis: verum

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; :: thesis: 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 ; :: thesis: 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; :: 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

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; :: thesis: verum