let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being FinPartState of S holds
( p is pre-program of S iff p computes {} .--> {} )
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N
for p being FinPartState of S holds
( p is pre-program of S iff p computes {} .--> {} )
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of IL,N; :: thesis: for p being FinPartState of S holds
( p is pre-program of S iff p computes {} .--> {} )
let p be FinPartState of S; :: thesis: ( p is pre-program of S iff p computes {} .--> {} )
thus ( p is pre-program of S implies p computes {} .--> {} ) :: thesis: ( p computes {} .--> {} implies p is pre-program of S )

proof

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

end;

dom ({} .--> {} ) = {{} } by FUNCOP_1:19;
then A4: {} in dom ({} .--> {} ) by TARSKI:def 1;
assume p computes {} .--> {} ; :: thesis: p is pre-program of S
then consider s being FinPartState of S such that
A5: s = {} and
A6: p +* s is pre-program of S and
({} .--> {} ) . s c= Result (p +* s) by A4, Def29;
thus p is pre-program of S by A5, A6, FUNCT_4:22; :: thesis: verum