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