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 is pre-program of S iff 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 is pre-program of S iff p,d computes {} .--> {} )
let p be NAT -defined the Instructions of S -valued Function; :: thesis: for d being FinPartState of S holds
( p +* d is pre-program of S iff p,d computes {} .--> {} )
let d be FinPartState of S; :: thesis: ( p +* d is pre-program of S iff p,d computes {} .--> {} )
thus ( p +* d is pre-program of S implies p,d computes {} .--> {} ) :: thesis: ( p,d computes {} .--> {} implies p +* d is pre-program of S )

proof

A1: dom ({} .--> {} ) = {{} } by FUNCOP_1:19;
assume A2: p +* d is pre-program 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 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 A3: x = {} by A1, TARSKI:def 1;
then reconsider s = x as FinPartState of S by FUNCT_1:174, RELAT_1:206;
take s ; :: thesis: ( x = s & (p +* d) +* s is pre-program of S & ({} .--> {} ) . s c= Result p,(d +* s) )
thus x = s ; :: thesis: ( (p +* d) +* s is pre-program of S & ({} .--> {} ) . s c= Result p,(d +* s) )
thus (p +* d) +* s is pre-program of S by A2, A3, FUNCT_4:22; :: thesis: ({} .--> {} ) . s c= Result p,(d +* s)
({} .--> {} ) . s = {} by A3, FUNCOP_1:87;
hence ({} .--> {} ) . s c= Result p,(d +* s) by XBOOLE_1:2; :: thesis: verum

end;

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