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 {} .--> (Result p,d) )
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 {} .--> (Result p,d) )
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 {} .--> (Result p,d) )
let d be FinPartState of S; :: thesis: ( p +* d is pre-program of S iff p,d computes {} .--> (Result p,d) )
thus ( p +* d is pre-program of S implies p,d computes {} .--> (Result p,d) ) :: thesis: ( p,d computes {} .--> (Result p,d) implies p +* d is pre-program of S )

proof

A1: dom ({} .--> (Result p,d)) = {{} } by FUNCOP_1:19;
assume A2: p +* d is pre-program of S ; :: thesis: p,d computes {} .--> (Result p,d)
let x be set ; :: according to AMI_1:def 30 :: thesis: ( x in dom ({} .--> (Result p,d)) implies ex s being FinPartState of S st
( x = s & (p +* d) +* s is pre-program of S & ({} .--> (Result p,d)) . s c= Result p,(d +* s) ) )
assume x in dom ({} .--> (Result p,d)) ; :: thesis: ex s being FinPartState of S st
( x = s & (p +* d) +* s is pre-program of S & ({} .--> (Result p,d)) . 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 & ({} .--> (Result p,d)) . s c= Result p,(d +* s) )
thus x = s ; :: thesis: ( (p +* d) +* s is pre-program of S & ({} .--> (Result p,d)) . s c= Result p,(d +* s) )
thus (p +* d) +* s is pre-program of S by A2, A3, FUNCT_4:22; :: thesis: ({} .--> (Result p,d)) . s c= Result p,(d +* s)
X: d +* s = d by A3, FUNCT_4:22;
({} .--> (Result p,d)) . s = Result p,d by A3, FUNCOP_1:87;
hence ({} .--> (Result p,d)) . s c= Result p,(d +* s) by X; :: thesis: verum

end;

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