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 p,d computes {}
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 p,d computes {}
let p be NAT -defined the Instructions of S -valued non halt-free Function; :: thesis: for d being FinPartState of S holds p,d computes {}
let d be FinPartState of S; :: thesis: p,d computes {}
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 A1: 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 reconsider x = x as FinPartState of S ;
take x ; :: thesis: ( x = x & d +* x is Autonomy of p & {} . x c= Result (p,(d +* x)) )
thus ( x = x & d +* x is Autonomy of p & {} . x c= Result (p,(d +* x)) ) by A1; :: thesis: verum