let j, k be natural number ; :: thesis: for R being good Ring
for I being Instruction of (SCM R)
for s being State of (SCM R) st IC s = il. (SCM R),(j + k) holds
Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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 = il. (SCM R),(j + k) holds
Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))
let I be Instruction of (SCM R); :: thesis: for s being State of (SCM R) st IC s = il. (SCM R),(j + k) holds
Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))
let s be State of (SCM R); :: thesis: ( IC s = il. (SCM R),(j + k) implies Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) )
A1: now
let d be Element of NAT ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . d
thus (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) . d by AMI_1:def 13
.= s . d by AMI_1:112
.= (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)),(SCM R))) . d by AMI_1:112 ; :: thesis: verum
end;
assume A2: IC s = il. (SCM R),(j + k) ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))
then A3: succ ((IC s) -' k,(SCM R)) = succ (((il. (SCM R),j) + k,(SCM R)) -' k,(SCM R)) by AMISTD_1:def 13
.= succ (il. (SCM R),j) by AMISTD_1:61
.= il. (SCM R),(j + 1) by SCMRING3:67
.= ((il. (SCM R),(j + 1)) + k,(SCM R)) -' k,(SCM R) by AMISTD_1:61
.= (il. (SCM R),((j + 1) + k)) -' k,(SCM R) by AMISTD_1:def 13
.= (il. (SCM R),((j + k) + 1)) -' k,(SCM R)
.= (succ (IC s)) -' k,(SCM R) by A2, SCMRING3:67 ;
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)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))
then A4: I = halt (SCM R) by SCMRING3:16;
hence Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)) by AMI_1:def 8
.= s +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) by A4, AMI_1:def 8
.= (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A10: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) by A5, SCMRING2:13
.= (IC (Exec (IncAddr I,k),s)) -' k,(SCM R) by A3, A7, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) by A1, A8, Th21; :: thesis: verum
end;
suppose InsCode I = 2 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = ((s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) . da) + ((s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) . db) by A11, SCMRING2:14
.= (s . da) + ((s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A16: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) by A11, SCMRING2:14
.= (IC (Exec (IncAddr I,k),s)) -' k,(SCM R) by A3, A13, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) by A1, A14, Th21; :: thesis: verum
end;
suppose InsCode I = 3 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = ((s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) . da) - ((s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) . db) by A17, SCMRING2:15
.= (s . da) - ((s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A22: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) by A17, SCMRING2:15
.= (IC (Exec (IncAddr I,k),s)) -' k,(SCM R) by A3, A19, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) by A1, A20, Th21; :: thesis: verum
end;
suppose InsCode I = 4 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = ((s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) . da) * ((s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) . db) by A23, SCMRING2:16
.= (s . da) * ((s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A28: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) by A23, SCMRING2:16
.= (IC (Exec (IncAddr I,k),s)) -' k,(SCM R) by A3, A25, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) by A1, A26, Th21; :: thesis: verum
end;
suppose InsCode I = 5 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
suppose A34: da <> d ; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . b1 = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . b1
hence (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ;
:: thesis: verum
end;
end;
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) by A29, SCMRING2:19
.= (IC (Exec (IncAddr I,k),s)) -' k,(SCM R) by A3, A31, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) by A1, A32, Th21; :: thesis: verum
end;
suppose InsCode I = 6 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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,(SCM R)),R by A35, SCMRING3:69;
then A37: IC (Exec (IncAddr I,k),s) = loc + k,(SCM R) by SCMRING2:17;
A38: now
let d be Data-Location of R; :: thesis: (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . d
thus (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ; :: thesis: verum
end;
IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = loc by A35, SCMRING2:17
.= (IC (Exec (IncAddr I,k),s)) -' k,(SCM R) by A37, AMISTD_1:61
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) by AMI_1:111 ;
hence Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) by A1, A38, Th21; :: thesis: verum
end;
suppose InsCode I = 7 ; :: thesis: Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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,(SCM R)) 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)),(SCM R)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)))
then A43: IC (Exec (IncAddr I,k),s) = loc + k,(SCM R) by A40, SCMRING2:18;
(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) . da = 0. R by A42, Th20;
then IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = loc by A39, SCMRING2:18
.= (IC (Exec (IncAddr I,k),s)) -' k,(SCM R) by A43, AMISTD_1:61
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) by AMI_1:111 ;
hence IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) ; :: thesis: verum
end;
suppose A44: s . da <> 0. R ; :: thesis: IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R))) . da <> 0. R by A44, Th20;
then IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = succ (IC (s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) by A39, SCMRING2:18
.= (IC (Exec (IncAddr I,k),s)) -' k,(SCM R) by A3, A45, AMI_1:111
.= IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) by AMI_1:111 ;
hence IC (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) = IC ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(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)),(SCM R)))) . d = ((Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R))) . d
thus (Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R)))) . d = (s +* (Start-At ((IC s) -' k,(SCM R)),(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)),(SCM R))) . d by Th20 ; :: thesis: verum
end;
hence Exec I,(s +* (Start-At ((IC s) -' k,(SCM R)),(SCM R))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k,(SCM R)),(SCM R)) by A1, A41, Th21; :: thesis: verum
end;
end;