let N be non empty with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for p being NAT -defined the InstructionsF of b1 -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> {} )

let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N; :: thesis: for p being NAT -defined the InstructionsF of S -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> {} )

let p be NAT -defined the InstructionsF of S -valued non halt-free Function; :: thesis: for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> {} )

let d be FinPartState of S; :: thesis: ( d is Autonomy of p iff p,d computes {} .--> {} )
thus ( d is Autonomy of p implies p,d computes {} .--> {} ) :: thesis: ( p,d computes {} .--> {} implies d is Autonomy of p )
proof
assume A2: d is Autonomy of p ; :: thesis:
let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( x in dom () implies ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & () . s c= Result (p,(d +* s)) ) )

assume A3: x in dom () ; :: thesis: ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & () . s c= Result (p,(d +* s)) )

then x = {} by TARSKI:def 1;
then reconsider s = x as FinPartState of S by ;
take s ; :: thesis: ( x = s & d +* s is Autonomy of p & () . s c= Result (p,(d +* s)) )
A5: d +* {} = d ;
thus x = s ; :: thesis: ( d +* s is Autonomy of p & () . s c= Result (p,(d +* s)) )
thus d +* s is Autonomy of p by ; :: thesis: () . s c= Result (p,(d +* s))
({} .--> {}) . s = {} ;
hence ({} .--> {}) . s c= Result (p,(d +* s)) by XBOOLE_1:2; :: thesis: verum
end;
A6: {} in dom () by TARSKI:def 1;
assume p,d computes {} .--> {} ; :: thesis: d is Autonomy of p
then ex s being FinPartState of S st
( {} = s & d +* s is Autonomy of p & () . s c= Result (p,(d +* s)) ) by A6;
hence d is Autonomy of p ; :: thesis: verum