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 P being Instruction-Sequence of S st F c= P holds

for k being Nat holds IC (Comput (P,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 P being Instruction-Sequence of S st F c= P holds

for k being Nat holds IC (Comput (P,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 P being Instruction-Sequence of S st F c= P holds

for k being Nat holds IC (Comput (P,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 P being Instruction-Sequence of S st F c= P holds

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

for P being Instruction-Sequence of S st F c= P holds

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

for P being Instruction-Sequence of S st F c= P holds

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

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

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 P being Instruction-Sequence of S st F c= P holds

for k being Nat holds IC (Comput (P,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 P being Instruction-Sequence of S st F c= P holds

for k being Nat holds IC (Comput (P,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 P being Instruction-Sequence of S st F c= P holds

for k being Nat holds IC (Comput (P,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 P being Instruction-Sequence of S st F c= P holds

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

for P being Instruction-Sequence of S st F c= P holds

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

proof

assume A9:
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 P being Instruction-Sequence of S st F c= P holds

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

let s be State of S; :: thesis: ( IC s in dom F implies for P being Instruction-Sequence of S st F c= P holds

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

assume A2: IC s in dom F ; :: thesis: for P being Instruction-Sequence of S st F c= P holds

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

let P be Instruction-Sequence of S; :: thesis: ( F c= P implies for k being Nat holds IC (Comput (P,s,k)) in dom F )

assume A3: F c= P ; :: thesis: for k being Nat holds IC (Comput (P,s,k)) in dom F

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

_{1}[ 0 ]
by A2;

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

end;for P being Instruction-Sequence of S st F c= P holds

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

let s be State of S; :: thesis: ( IC s in dom F implies for P being Instruction-Sequence of S st F c= P holds

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

assume A2: IC s in dom F ; :: thesis: for P being Instruction-Sequence of S st F c= P holds

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

let P be Instruction-Sequence of S; :: thesis: ( F c= P implies for k being Nat holds IC (Comput (P,s,k)) in dom F )

assume A3: F c= P ; :: thesis: for k being Nat holds IC (Comput (P,s,k)) in dom F

defpred S

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

S_{1}[k + 1]

A8:
SS

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

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

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

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

A6: IC (Following (P,t)) in NIC ((P /. (IC (Comput (P,s,k)))),(IC (Comput (P,s,k)))) ;

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

P /. (IC (Comput (P,s,k))) = F /. (IC (Comput (P,s,k))) by A5, A3, PARTFUN2:61;

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

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

end;assume A5: S

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

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

A6: IC (Following (P,t)) in NIC ((P /. (IC (Comput (P,s,k)))),(IC (Comput (P,s,k)))) ;

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

P /. (IC (Comput (P,s,k))) = F /. (IC (Comput (P,s,k))) by A5, A3, PARTFUN2:61;

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

hence S

thus for k being Nat holds S

for P being Instruction-Sequence of S st F c= P holds

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

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

proof

hence
F is really-closed
by Th14; :: thesis: verum
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 A10: IC s in dom F ; :: thesis: for k being Nat holds IC (Comput (F,s,k)) in dom F

consider P being Instruction-Sequence of S such that

A11: F c= P by PBOOLE:145;

let k be Nat; :: thesis: IC (Comput (F,s,k)) in dom F

A12: IC (Comput (P,s,k)) in dom F by A9, A10, A11;

defpred S_{1}[ Nat] means Comput (P,s,$1) = Comput (F,s,$1);

A13: S_{1}[ 0 ]
;

A14: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A13, A14);

hence IC (Comput (F,s,k)) in dom F by A12; :: thesis: verum

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

consider P being Instruction-Sequence of S such that

A11: F c= P by PBOOLE:145;

let k be Nat; :: thesis: IC (Comput (F,s,k)) in dom F

A12: IC (Comput (P,s,k)) in dom F by A9, A10, A11;

defpred S

A13: S

A14: for k being Nat st S

S

proof

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

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

reconsider kk = k as Nat ;

A16: IC (Comput (P,s,kk)) in dom F by A9, A10, A11;

Comput (P,s,(k + 1)) = Following (P,(Comput (F,s,k))) by A15, EXTPRO_1:3

.= Following (F,(Comput (F,s,k))) by A16, A11, A15, PARTFUN2:61

.= Comput (F,s,(k + 1)) by EXTPRO_1:3 ;

hence S_{1}[k + 1]
; :: thesis: verum

end;assume A15: S

reconsider kk = k as Nat ;

A16: IC (Comput (P,s,kk)) in dom F by A9, A10, A11;

Comput (P,s,(k + 1)) = Following (P,(Comput (F,s,k))) by A15, EXTPRO_1:3

.= Following (F,(Comput (F,s,k))) by A16, A11, A15, PARTFUN2:61

.= Comput (F,s,(k + 1)) by EXTPRO_1:3 ;

hence S

hence IC (Comput (F,s,k)) in dom F by A12; :: thesis: verum