let N be with_zero set ; 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; 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; ( 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 )
( ( 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 A1:
F is
really-closed
;
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;
( 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
;
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;
( F c= P implies for k being Nat holds IC (Comput (P,s,k)) in dom F )
assume A3:
F c= P
;
for k being Nat holds IC (Comput (P,s,k)) in dom F
defpred S1[
Nat]
means IC (Comput (P,s,$1)) in dom F;
A4:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A5:
S1[
k]
;
S1[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
S1[
k + 1]
by A6, A7;
verum end;
A8:
S1[
0 ]
by A2;
thus
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A8, A4); verum
end;
assume A9:
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
; 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
let s be
State of
S;
( 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
;
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;
IC (Comput (F,s,k)) in dom F
A12:
IC (Comput (P,s,k)) in dom F
by A9, A10, A11;
defpred S1[
Nat]
means Comput (
P,
s,$1)
= Comput (
F,
s,$1);
A13:
S1[
0 ]
;
A14:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A15:
S1[
k]
;
S1[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
S1[
k + 1]
;
verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A13, A14);
hence
IC (Comput (F,s,k)) in dom F
by A12;
verum
end;
hence
F is really-closed
by Th14; verum