let j, k be Element of NAT ; :: thesis: for R being good Ring
for I being Instruction of (SCM R)
for s being State of (SCM R) st IC s = j + k holds
Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
let R be good Ring; :: thesis: for I being Instruction of (SCM R)
for s being State of (SCM R) st IC s = j + k holds
Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
let I be Instruction of (SCM R); :: thesis: for s being State of (SCM R) st IC s = j + k holds
Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
let s be State of (SCM R); :: thesis: ( IC s = j + k implies Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) )
A1: now
let d be Element of NAT ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d
thus (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . d by AMI_1:def 13
.= s . d by COMPOS_1:20
.= (Exec (IncAddr I,k),s) . d by AMI_1:def 13
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by COMPOS_1:20 ; :: thesis: verum
end;
assume A2: IC s = j + k ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then A3: succ ((IC s) -' k) = succ j by NAT_D:34
.= ((j + 1) + k) -' k by NAT_D:34
.= (succ (IC s)) -' k by A2 ;
per cases ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 ) by NAT_1:32, SCMRING3:71;
suppose InsCode I = 0 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then A4: I = halt (SCM R) by SCMRING3:16;
hence Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = s +* (Start-At ((IC s) -' k),(SCM R)) by AMI_1:def 8
.= s +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A4, AMI_1:def 8
.= (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A4, AMI_1:def 8 ;
:: thesis: verum
end;
suppose InsCode I = 1 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then consider da, db being Data-Location of R such that
A5: I = da := db by SCMRING3:17;
A6: IncAddr I,k = da := db by A5, AMISTD_2:29;
then A7: (Exec (IncAddr I,k),s) . (IC (SCM R)) = succ (IC s) by SCMRING2:13;
A8: now
let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
per cases ( da = d or da <> d ) ;
suppose A9: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . db by A5, SCMRING2:13
.= s . db by Th20
.= (Exec (IncAddr I,k),s) . d by A6, A9, SCMRING2:13
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A10: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . d by A5, SCMRING2:13
.= s . d by Th20
.= (Exec (IncAddr I,k),s) . d by A6, A10, SCMRING2:13
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k),(SCM R)))) by A5, SCMRING2:13
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A7, FUNCT_4:121
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) by FUNCT_4:121 ;
hence Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A1, A8, Th21; :: thesis: verum
end;
suppose InsCode I = 2 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then consider da, db being Data-Location of R such that
A11: I = AddTo da,db by SCMRING3:18;
A12: IncAddr I,k = AddTo da,db by A11, AMISTD_2:29;
then A13: (Exec (IncAddr I,k),s) . (IC (SCM R)) = succ (IC s) by SCMRING2:14;
A14: now
let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
per cases ( da = d or da <> d ) ;
suppose A15: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = ((s +* (Start-At ((IC s) -' k),(SCM R))) . da) + ((s +* (Start-At ((IC s) -' k),(SCM R))) . db) by A11, SCMRING2:14
.= (s . da) + ((s +* (Start-At ((IC s) -' k),(SCM R))) . db) by Th20
.= (s . da) + (s . db) by Th20
.= (Exec (IncAddr I,k),s) . d by A12, A15, SCMRING2:14
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A16: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . d by A11, SCMRING2:14
.= s . d by Th20
.= (Exec (IncAddr I,k),s) . d by A12, A16, SCMRING2:14
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k),(SCM R)))) by A11, SCMRING2:14
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A13, FUNCT_4:121
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) by FUNCT_4:121 ;
hence Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A1, A14, Th21; :: thesis: verum
end;
suppose InsCode I = 3 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then consider da, db being Data-Location of R such that
A17: I = SubFrom da,db by SCMRING3:19;
A18: IncAddr I,k = SubFrom da,db by A17, AMISTD_2:29;
then A19: (Exec (IncAddr I,k),s) . (IC (SCM R)) = succ (IC s) by SCMRING2:15;
A20: now
let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
per cases ( da = d or da <> d ) ;
suppose A21: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = ((s +* (Start-At ((IC s) -' k),(SCM R))) . da) - ((s +* (Start-At ((IC s) -' k),(SCM R))) . db) by A17, SCMRING2:15
.= (s . da) - ((s +* (Start-At ((IC s) -' k),(SCM R))) . db) by Th20
.= (s . da) - (s . db) by Th20
.= (Exec (IncAddr I,k),s) . d by A18, A21, SCMRING2:15
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A22: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . d by A17, SCMRING2:15
.= s . d by Th20
.= (Exec (IncAddr I,k),s) . d by A18, A22, SCMRING2:15
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k),(SCM R)))) by A17, SCMRING2:15
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A19, FUNCT_4:121
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) by FUNCT_4:121 ;
hence Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A1, A20, Th21; :: thesis: verum
end;
suppose InsCode I = 4 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then consider da, db being Data-Location of R such that
A23: I = MultBy da,db by SCMRING3:20;
A24: IncAddr I,k = MultBy da,db by A23, AMISTD_2:29;
then A25: (Exec (IncAddr I,k),s) . (IC (SCM R)) = succ (IC s) by SCMRING2:16;
A26: now
let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
per cases ( da = d or da <> d ) ;
suppose A27: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = ((s +* (Start-At ((IC s) -' k),(SCM R))) . da) * ((s +* (Start-At ((IC s) -' k),(SCM R))) . db) by A23, SCMRING2:16
.= (s . da) * ((s +* (Start-At ((IC s) -' k),(SCM R))) . db) by Th20
.= (s . da) * (s . db) by Th20
.= (Exec (IncAddr I,k),s) . d by A24, A27, SCMRING2:16
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A28: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . d by A23, SCMRING2:16
.= s . d by Th20
.= (Exec (IncAddr I,k),s) . d by A24, A28, SCMRING2:16
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k),(SCM R)))) by A23, SCMRING2:16
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A25, FUNCT_4:121
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) by FUNCT_4:121 ;
hence Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A1, A26, Th21; :: thesis: verum
end;
suppose InsCode I = 5 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then consider da being Data-Location of R, r being Element of R such that
A29: I = da := r by SCMRING3:21;
A30: IncAddr I,k = da := r by A29, AMISTD_2:29;
then A31: (Exec (IncAddr I,k),s) . (IC (SCM R)) = succ (IC s) by SCMRING2:19;
A32: now
let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
per cases ( da = d or da <> d ) ;
suppose A33: da = d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = r by A29, SCMRING2:19
.= (Exec (IncAddr I,k),s) . d by A30, A33, SCMRING2:19
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A34: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . d by A29, SCMRING2:19
.= s . d by Th20
.= (Exec (IncAddr I,k),s) . d by A30, A34, SCMRING2:19
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k),(SCM R)))) by A29, SCMRING2:19
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A31, FUNCT_4:121
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) by FUNCT_4:121 ;
hence Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A1, A32, Th21; :: thesis: verum
end;
suppose InsCode I = 6 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then consider loc being Element of NAT such that
A35: I = goto loc,R by SCMRING3:22;
A36: IncAddr I,k = goto (loc + k),R by A35, SCMRING3:69;
then A37: IC (Exec (IncAddr I,k),s) = loc + k by SCMRING2:17;
A38: now
let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d
thus (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . d by A35, SCMRING2:17
.= s . d by Th20
.= (Exec (IncAddr I,k),s) . d by A36, SCMRING2:17
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ; :: thesis: verum
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = loc by A35, SCMRING2:17
.= (IC (Exec (IncAddr I,k),s)) -' k by A37, NAT_D:34
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) by FUNCT_4:121 ;
hence Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A1, A38, Th21; :: thesis: verum
end;
suppose InsCode I = 7 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))
then consider da being Data-Location of R, loc being Element of NAT such that
A39: I = da =0_goto loc by SCMRING3:23;
A40: IncAddr I,k = da =0_goto (loc + k) by A39, SCMRING3:70;
A41: now
per cases ( s . da = 0. R or s . da <> 0. R ) ;
suppose A42: s . da = 0. R ; :: thesis: IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)))
then A43: IC (Exec (IncAddr I,k),s) = loc + k by A40, SCMRING2:18;
(s +* (Start-At ((IC s) -' k),(SCM R))) . da = 0. R by A42, Th20;
then IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = loc by A39, SCMRING2:18
.= (IC (Exec (IncAddr I,k),s)) -' k by A43, NAT_D:34
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) by FUNCT_4:121 ;
hence IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) ; :: thesis: verum
end;
suppose A44: s . da <> 0. R ; :: thesis: IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)))
then A45: (Exec (IncAddr I,k),s) . (IC (SCM R)) = succ (IC s) by A40, SCMRING2:18;
(s +* (Start-At ((IC s) -' k),(SCM R))) . da <> 0. R by A44, Th20;
then IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k),(SCM R)))) by A39, SCMRING2:18
.= (IC (Exec (IncAddr I,k),s)) -' k by A3, A45, FUNCT_4:121
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) by FUNCT_4:121 ;
hence IC (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) ; :: thesis: verum
end;
end;
end;
now
let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d
thus (Exec I,(s +* (Start-At ((IC s) -' k),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k),(SCM R))) . d by A39, SCMRING2:18
.= s . d by Th20
.= (Exec (IncAddr I,k),s) . d by A40, SCMRING2:18
.= ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R))) . d by Th20 ; :: thesis: verum
end;
hence Exec I,(s +* (Start-At ((IC s) -' k),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k),(SCM R)) by A1, A41, Th21; :: thesis: verum
end;
end;