let I be Program of ; :: thesis: ( I is paraclosed iff for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P )
thus ( I is paraclosed implies for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P ) by FUNCT_4:25; :: thesis: ( ( for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P ) implies I is paraclosed )
assume A1: for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P ; :: thesis: I is paraclosed
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 6 :: thesis: for b₁ being set
for b₂ being set holds
( not stop I c= b₂ or IC (Comput (b₂,s,b₁)) in K238((stop I)) )
let k be Nat; :: thesis: for b₁ being set holds
( not stop I c= b₁ or IC (Comput (b₁,s,k)) in K238((stop I)) )
let P be Instruction-Sequence of SCMPDS; :: thesis: ( not stop I c= P or IC (Comput (P,s,k)) in K238((stop I)) )
A2: Initialize s = s by MEMSTR_0:44;
assume stop I c= P ; :: thesis: IC (Comput (P,s,k)) in K238((stop I))
then A3: P = P +* (stop I) by FUNCT_4:98;
I is_closed_on s,P by A1;
hence IC (Comput (P,s,k)) in dom (stop I) by A2, A3; :: thesis: verum