let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N
for p being NAT -defined the Instructions of b₁ -valued Function
for d being FinPartState of S holds p,d computes {}
let S be non empty stored-program IC-Ins-separated definite realistic halting steady-programmed AMI-Struct of N; :: thesis: for p being NAT -defined the Instructions of S -valued Function
for d being FinPartState of S holds p,d computes {}
let p be NAT -defined the Instructions of S -valued 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 AMI_1:def 30 :: thesis: ( x in dom {} implies ex s being FinPartState of S st
( x = s & (p +* d) +* s is pre-program of S & {} . s c= Result p,(d +* s) ) )
assume A1: x in dom {} ; :: thesis: ex s being FinPartState of S st
( x = s & (p +* d) +* s is pre-program of S & {} . s c= Result p,(d +* s) )
then reconsider x = x as FinPartState of S ;
take x ; :: thesis: ( x = x & (p +* d) +* x is pre-program of S & {} . x c= Result p,(d +* x) )
thus ( x = x & (p +* d) +* x is pre-program of S & {} . x c= Result p,(d +* x) ) by A1; :: thesis: verum