let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for F being preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F )

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for F being preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F )

let F be preProgram of S; :: thesis: ( F is really-closed iff for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F )

thus ( F is really-closed implies for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F ) :: thesis: ( ( for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F ) implies F is really-closed )

for k being Nat holds IC (Comput (F,s,k)) in dom F ; :: thesis: F is really-closed

let l be Nat; :: according to AMISTD_1:def 9 :: thesis: ( l in dom F implies NIC ((F /. l),l) c= dom F )

assume A9: l in dom F ; :: thesis: NIC ((F /. l),l) c= dom F

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC ((F /. l),l) or x in dom F )

assume x in NIC ((F /. l),l) ; :: thesis: x in dom F

then consider ss being Element of product (the_Values_of S) such that

A10: x = IC (Exec ((F /. l),ss)) and

A11: IC ss = l ;

reconsider ss = ss as State of S ;

IC (Comput (F,ss,(0 + 1))) = IC (Following (F,(Comput (F,ss,0)))) by EXTPRO_1:3

.= IC (Following (F,ss))

.= IC (Exec ((F /. (IC ss)),ss)) ;

hence x in dom F by A10, A11, A8, A9; :: thesis: verum

for F being preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F )

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for F being preProgram of S holds

( F is really-closed iff for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F )

let F be preProgram of S; :: thesis: ( F is really-closed iff for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F )

thus ( F is really-closed implies for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F ) :: thesis: ( ( for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F ) implies F is really-closed )

proof

assume A8:
for s being State of S st IC s in dom F holds
assume A1:
F is really-closed
; :: thesis: for s being State of S st IC s in dom F holds

for k being Nat holds IC (Comput (F,s,k)) in dom F

let s be State of S; :: thesis: ( IC s in dom F implies for k being Nat holds IC (Comput (F,s,k)) in dom F )

assume A2: IC s in dom F ; :: thesis: for k being Nat holds IC (Comput (F,s,k)) in dom F

defpred S_{1}[ Nat] means IC (Comput (F,s,$1)) in dom F;

_{1}[ 0 ]
by A2;

thus for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A7, A3); :: thesis: verum

end;for k being Nat holds IC (Comput (F,s,k)) in dom F

let s be State of S; :: thesis: ( IC s in dom F implies for k being Nat holds IC (Comput (F,s,k)) in dom F )

assume A2: IC s in dom F ; :: thesis: for k being Nat holds IC (Comput (F,s,k)) in dom F

defpred S

A3: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A7:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

reconsider t = Comput (F,s,k) as Element of product (the_Values_of S) by CARD_3:107;

set l = IC (Comput (F,s,k));

A5: IC (Following (F,t)) in NIC ((F /. (IC (Comput (F,s,k)))),(IC (Comput (F,s,k)))) ;

A6: Comput (F,s,(k + 1)) = Following (F,t) by EXTPRO_1:3;

NIC ((F /. (IC (Comput (F,s,k)))),(IC (Comput (F,s,k)))) c= dom F by A1, A4;

hence S_{1}[k + 1]
by A5, A6; :: thesis: verum

end;assume A4: S

reconsider t = Comput (F,s,k) as Element of product (the_Values_of S) by CARD_3:107;

set l = IC (Comput (F,s,k));

A5: IC (Following (F,t)) in NIC ((F /. (IC (Comput (F,s,k)))),(IC (Comput (F,s,k)))) ;

A6: Comput (F,s,(k + 1)) = Following (F,t) by EXTPRO_1:3;

NIC ((F /. (IC (Comput (F,s,k)))),(IC (Comput (F,s,k)))) c= dom F by A1, A4;

hence S

thus for k being Nat holds S

for k being Nat holds IC (Comput (F,s,k)) in dom F ; :: thesis: F is really-closed

let l be Nat; :: according to AMISTD_1:def 9 :: thesis: ( l in dom F implies NIC ((F /. l),l) c= dom F )

assume A9: l in dom F ; :: thesis: NIC ((F /. l),l) c= dom F

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC ((F /. l),l) or x in dom F )

assume x in NIC ((F /. l),l) ; :: thesis: x in dom F

then consider ss being Element of product (the_Values_of S) such that

A10: x = IC (Exec ((F /. l),ss)) and

A11: IC ss = l ;

reconsider ss = ss as State of S ;

IC (Comput (F,ss,(0 + 1))) = IC (Following (F,(Comput (F,ss,0)))) by EXTPRO_1:3

.= IC (Following (F,ss))

.= IC (Exec ((F /. (IC ss)),ss)) ;

hence x in dom F by A10, A11, A8, A9; :: thesis: verum