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