let I be Program of SCMPDS; :: 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 )

hereby :: 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: I is paraclosed ; :: thesis: for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P
let s be State of SCMPDS; :: thesis: for P being Instruction-Sequence of SCMPDS holds I is_closed_on s,P
let P be Instruction-Sequence of SCMPDS; :: thesis: I is_closed_on s,P
stop I c= P +* (stop I) by FUNCT_4:25;
then for n being Element of NAT holds IC (Comput ((P +* (stop I)),(Initialize s),n)) in dom (stop I) by A1, SCMPDS_4:def 6;
hence I is_closed_on s,P by Def2; :: thesis: verum

end;

assume A2: 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 Element of NAT
for b₂ being set holds
( not stop I c= b₂ or IC (Comput (b₂,s,b₁)) in dom (stop I) )
let k be Element of NAT ; :: thesis: for b₁ being set holds
( not stop I c= b₁ or IC (Comput (b₁,s,k)) in dom (stop I) )
let P be Instruction-Sequence of SCMPDS; :: thesis: ( not stop I c= P or IC (Comput (P,s,k)) in dom (stop I) )
A3: Initialize s = s by MEMSTR_0:44;
assume stop I c= P ; :: thesis: IC (Comput (P,s,k)) in dom (stop I)
then A4: P = P +* (stop I) by FUNCT_4:98;
I is_closed_on s,P by A2;
hence IC (Comput (P,s,k)) in dom (stop I) by A3, A4, Def2; :: thesis: verum