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

( S is IC-recognized iff for q being NAT -defined the InstructionsF of b_{1} -valued finite non halt-free Function

for p being b_{2} -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p )

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: ( S is IC-recognized iff for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being b_{1} -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p )

thus ( S is IC-recognized implies for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being b_{1} -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p ) :: thesis: ( ( for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being b_{1} -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p ) implies S is IC-recognized )

for p being b_{1} -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p ; :: thesis: S is IC-recognized

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: according to AMISTD_5:def 3 :: thesis: for p being q -autonomic FinPartState of S st not p is empty holds

IC in dom p

let p be q -autonomic FinPartState of S; :: thesis: ( not p is empty implies IC in dom p )

A3: dom p c= {(IC )} \/ (dom (DataPart p)) by MEMSTR_0:32;

assume A4: not p is empty ; :: thesis: IC in dom p

( S is IC-recognized iff for q being NAT -defined the InstructionsF of b

for p being b

IC in dom p )

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: ( S is IC-recognized iff for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being b

IC in dom p )

thus ( S is IC-recognized implies for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being b

IC in dom p ) :: thesis: ( ( for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being b

IC in dom p ) implies S is IC-recognized )

proof

assume A2:
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
assume A1:
S is IC-recognized
; :: thesis: for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function

for p being b_{1} -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being q -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p

let p be q -autonomic FinPartState of S; :: thesis: ( DataPart p <> {} implies IC in dom p )

assume DataPart p <> {} ; :: thesis: IC in dom p

then not p is empty ;

hence IC in dom p by A1; :: thesis: verum

end;for p being b

IC in dom p

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: thesis: for p being q -autonomic FinPartState of S st DataPart p <> {} holds

IC in dom p

let p be q -autonomic FinPartState of S; :: thesis: ( DataPart p <> {} implies IC in dom p )

assume DataPart p <> {} ; :: thesis: IC in dom p

then not p is empty ;

hence IC in dom p by A1; :: thesis: verum

for p being b

IC in dom p ; :: thesis: S is IC-recognized

let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function; :: according to AMISTD_5:def 3 :: thesis: for p being q -autonomic FinPartState of S st not p is empty holds

IC in dom p

let p be q -autonomic FinPartState of S; :: thesis: ( not p is empty implies IC in dom p )

A3: dom p c= {(IC )} \/ (dom (DataPart p)) by MEMSTR_0:32;

assume A4: not p is empty ; :: thesis: IC in dom p