let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N
for p being FinPartState of S holds p computes {}
let S be non empty stored-program halting IC-Ins-separated steady-programmed definite realistic AMI-Struct of N; :: thesis: for p being FinPartState of S holds p computes {}
let p be FinPartState of S; :: thesis: p computes {}
let x be set ; :: according to AMI_1:def 29 :: thesis: ( x in dom {} implies ex s being FinPartState of S st
( x = s & p +* s is pre-program of S & {} . s c= Result (p +* s) ) )
assume A1: x in dom {} ; :: thesis: ex s being FinPartState of S st
( x = s & p +* s is pre-program of S & {} . s c= Result (p +* s) )
then reconsider x = x as FinPartState of S ;
take x ; :: thesis: ( x = x & p +* x is pre-program of S & {} . x c= Result (p +* x) )
thus ( x = x & p +* x is pre-program of S & {} . x c= Result (p +* x) ) by A1; :: thesis: verum