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

proof

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

end;

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