let I be Program of SCMPDS; :: thesis: ( I is paraclosed iff for s being State of SCMPDS holds I is_closed_on s )

hereby :: thesis: ( ( for s being State of SCMPDS holds I is_closed_on s ) implies I is paraclosed )

assume A1: I is paraclosed ; :: thesis: for s being State of SCMPDS holds I is_closed_on s
let s be State of SCMPDS; :: thesis: I is_closed_on s
stop I c= (Initialize s) +* (stop I) by FUNCT_4:26;
then for n being Element of NAT holds IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),n)) in dom (stop I) by A1, SCMPDS_4:def 9;
hence I is_closed_on s by Def2; :: thesis: verum

end;

assume A2: for s being State of SCMPDS holds I is_closed_on s ; :: thesis: I is paraclosed
let s be 0 -started State of SCMPDS; :: according to SCMPDS_4:def 9 :: thesis: for b₁ being Element of NAT holds
( not stop I c= s or IC (Comput ((ProgramPart s),s,b₁)) in dom (stop I) )
let k be Element of NAT ; :: thesis: ( not stop I c= s or IC (Comput ((ProgramPart s),s,k)) in dom (stop I) )
AA: Initialize s = s by COMPOS_1:78;
assume stop I c= s ; :: thesis: IC (Comput ((ProgramPart s),s,k)) in dom (stop I)
then A3: s = (Initialize s) +* (stop I) by AA, FUNCT_4:79;
I is_closed_on s by A2;
hence IC (Comput ((ProgramPart s),s,k)) in dom (stop I) by A3, Def2; :: thesis: verum