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 b_{1} -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 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 {} .--> (Result (p,d)) )

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 {} .--> (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 )

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 A5;

hence d is Autonomy of p ; :: thesis: verum

for p being NAT -defined the InstructionsF of b

for d being FinPartState of S holds

( d is Autonomy of p iff p,d computes {} .--> (Result (p,d)) )

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 {} .--> (Result (p,d)) )

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 {} .--> (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

A5:
{} in dom ({} .--> (Result (p,d)))
by TARSKI:def 1;
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 A3: 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 A4: x = {} by 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)) )

d +* {} = d ;

hence d +* s is Autonomy of p by A2, A3, TARSKI:def 1; :: thesis: ({} .--> (Result (p,d))) . s c= Result (p,(d +* s))

thus ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) by A4, FUNCOP_1:72; :: thesis: verum

end;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 A3: 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 A4: x = {} by 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)) )

d +* {} = d ;

hence d +* s is Autonomy of p by A2, A3, TARSKI:def 1; :: thesis: ({} .--> (Result (p,d))) . s c= Result (p,(d +* s))

thus ({} .--> (Result (p,d))) . s c= Result (p,(d +* s)) by A4, FUNCOP_1:72; :: thesis: verum

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 A5;

hence d is Autonomy of p ; :: thesis: verum