let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for t, u being State of S
for e being Element of NAT
for I being Instruction of S st u = t +* (((IC ),e) --> (e,I)) holds
( u . e = I & IC u = e & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) )
let S be non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for t, u being State of S
for e being Element of NAT
for I being Instruction of S st u = t +* (((IC ),e) --> (e,I)) holds
( u . e = I & IC u = e & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) )
let t, u be State of S; :: thesis: for e being Element of NAT
for I being Instruction of S st u = t +* (((IC ),e) --> (e,I)) holds
( u . e = I & IC u = e & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) )
let e be Element of NAT ; :: thesis: for I being Instruction of S st u = t +* (((IC ),e) --> (e,I)) holds
( u . e = I & IC u = e & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) )
let I be Instruction of S; :: thesis: ( u = t +* (((IC ),e) --> (e,I)) implies ( u . e = I & IC u = e & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) ) )
assume A1: u = t +* (((IC ),e) --> (e,I)) ; :: thesis: ( u . e = I & IC u = e & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) )
A2: dom (((IC ),e) --> (e,I)) = {(IC ),e} by FUNCT_4:65;
then e in dom (((IC ),e) --> (e,I)) by TARSKI:def 2;
hence u . e = (((IC ),e) --> (e,I)) . e by A1, FUNCT_4:14
.= I by FUNCT_4:66 ;
:: thesis: ( IC u = e & IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) )
reconsider il = e as Element of NAT ;
A3: IC <> il by COMPOS_1:def 12;
IC in dom (((IC ),e) --> (e,I)) by A2, TARSKI:def 2;
hence IC u = (((IC ),e) --> (e,I)) . (IC ) by A1, FUNCT_4:14
.= e by A3, FUNCT_4:66 ;
:: thesis: IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC )
thus IC (Following ((ProgramPart u),u)) = (Exec ((u . (IC u)),u)) . (IC ) by COMPOS_1:38; :: thesis: verum