let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated standard AMI-Struct of N
for F being NAT -defined the Instructions of b₁ -valued finite Function st F is really-closed & 0 in dom F holds
F is paraclosed
let S be non empty IC-Ins-separated standard AMI-Struct of N; :: thesis: for F being NAT -defined the Instructions of S -valued finite Function st F is really-closed & 0 in dom F holds
F is paraclosed
let F be NAT -defined the Instructions of S -valued finite Function; :: thesis: ( F is really-closed & 0 in dom F implies F is paraclosed )
assume Z: F is really-closed ; :: thesis: ( not 0 in dom F or F is paraclosed )
assume B1: 0 in dom F ; :: thesis: F is paraclosed
let s be 0 -started State of S; :: according to AMISTD_1:def 10 :: thesis: for P being Instruction-Sequence of S st F c= P holds
for k being Element of NAT holds IC (Comput (P,s,k)) in dom F
Z1: IC s = 0 by MEMSTR_0:def 8;
let P be Instruction-Sequence of S; :: thesis: ( F c= P implies for k being Element of NAT holds IC (Comput (P,s,k)) in dom F )
assume Z2: F c= P ; :: thesis: for k being Element of NAT holds IC (Comput (P,s,k)) in dom F
let k be Element of NAT ; :: thesis: IC (Comput (P,s,k)) in dom F
thus IC (Comput (P,s,k)) in dom F by Z, Z1, Z2, Lm45, B1; :: thesis: verum