let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated halting AMI-Struct of N
for p being NAT -defined the Instructions of b₁ -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
let S be non empty IC-Ins-separated halting AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued non halt-free Function
for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
let p be NAT -defined the Instructions of S -valued non halt-free Function; :: thesis: for d being FinPartState of S holds
( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
let d be FinPartState of S; :: thesis: ( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )
thus ( d is Autonomy of p implies p,d computes {} .--> (Result (p,d)) ) :: thesis: ( p,d computes {} .--> (Result (p,d)) implies d is Autonomy of p )

proof

A1: dom ({} .--> (Result (p,d))) = {{}} by FUNCOP_1:13;
assume A2: d is Autonomy of p ; :: thesis: p,d computes {} .--> (Result (p,d))
let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( x in dom ({} .--> (Result (p,d))) implies ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) )
assume x in dom ({} .--> (Result (p,d))) ; :: thesis: ex s being FinPartState of S st
( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) )
then A3: x = {} by A1, TARSKI:def 1;
then reconsider s = x as FinPartState of S by FUNCT_1:104, RELAT_1:171;
take s ; :: thesis: ( x = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) )
thus x = s ; :: thesis: ( d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) )
thus d +* s is Autonomy of p by A2, A3, FUNCT_4:21; :: thesis: ({} .--> (Result (p,d))) . s c= Result (p,(d +* s))
d +* s = d by A3, FUNCT_4:21;
hence ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) by A3, FUNCOP_1:72; :: thesis: verum

end;

dom ({} .--> (Result (p,d))) = {{}} by FUNCOP_1:13;
then A4: {} in dom ({} .--> (Result (p,d))) by TARSKI:def 1;
assume p,d computes {} .--> (Result (p,d)) ; :: thesis: d is Autonomy of p
then ex s being FinPartState of S st
( {} = s & d +* s is Autonomy of p & ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) ) by A4, Def13;
hence d is Autonomy of p by FUNCT_4:21; :: thesis: verum