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