let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for F being NAT -defined the InstructionsF of b₁ -valued finite Function st F is really-closed & 0 in dom F holds
F is paraclosed
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; :: thesis: for F being NAT -defined the InstructionsF of S -valued finite Function st F is really-closed & 0 in dom F holds
F is paraclosed
let F be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: ( F is really-closed & 0 in dom F implies F is paraclosed )
assume A1: F is really-closed ; :: thesis: ( not 0 in dom F or F is paraclosed )
assume A2: 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
A3: IC s = 0 by MEMSTR_0:def 11;
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 A4: 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 A1, A3, A4, Lm6, A2; :: thesis: verum