let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for p being NAT -defined the Instructions of b₁ -valued non halt-free Function
for d being program-free FinPartState of S holds ProgramPart (d +* p) = p
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued non halt-free Function
for d being program-free FinPartState of S holds ProgramPart (d +* p) = p
let p be NAT -defined the Instructions of S -valued non halt-free Function; :: thesis: for d being program-free FinPartState of S holds ProgramPart (d +* p) = p
let d be program-free FinPartState of S; :: thesis: ProgramPart (d +* p) = p
thus ProgramPart (d +* p) = (ProgramPart d) +* (p | NAT) by FUNCT_4:75
.= {} +* (p | NAT) by Def29
.= p | NAT by FUNCT_4:21
.= p by RELAT_1:209 ; :: thesis: verum