let k be Element of NAT ; :: thesis: for s being State of SCM holds Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
let s be State of SCM; :: thesis: Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
set INS = CurInstr ((ProgramPart s),s);
reconsider m = IC s as Element of NAT ;
A1: succ (IC (s +* (Start-At (((IC s) + k),SCM)))) = succ (m + k) by FUNCT_4:121
.= (m + k) + 1 by NAT_1:39
.= (m + 1) + k
.= (succ (IC s)) + k by NAT_1:39
.= IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) by FUNCT_4:121 ;
A2: now
let d be Element of NAT ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d
thus (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . 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))) . 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 or InsCode (CurInstr ((ProgramPart s),s)) = 8 ) by AMI_5:36, NAT_1:33;
suppose Z3: InsCode (CurInstr ((ProgramPart s),s)) = 0 ; :: thesis: Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then A3: CurInstr ((ProgramPart s),s) = halt SCM by AMI_5:46;
then A4: Following ((ProgramPart s),s) = s by EXTPRO_1:def 3;
X: IncAddr ((CurInstr ((ProgramPart s),s)),k) = CurInstr ((ProgramPart s),s) by A3, COMPOS_1:93;
thus Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = Exec ((halt SCM),(s +* (Start-At (((IC s) + k),SCM)))) by Z3, X, AMI_5:46
.= (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) by A4, 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)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then consider da, db being Data-Location such that
A5: CurInstr ((ProgramPart s),s) = da := db by AMI_5:47;
A6: now
let d be Data-Location ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
per cases ( da = d or da <> d ) ;
suppose A7: da = d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . db by A5, AMI_3:8
.= s . db by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A5, A7, AMI_3:8
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
suppose A8: da <> d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A5, AMI_3:8
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A5, A8, AMI_3:8
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
end;
end;
A9: IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) by A1, A5, AMI_3:8;
( IncAddr ((CurInstr ((ProgramPart s),s)),k) = CurInstr ((ProgramPart s),s) & IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = succ (IC s) ) by A5, AMI_3:8, COMPOS_1:92;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) by A2, A9, A6, AMI_5:26; :: 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)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then consider da, db being Data-Location such that
A10: CurInstr ((ProgramPart s),s) = AddTo (da,db) by AMI_5:48;
A11: now
let d be Data-Location ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
per cases ( da = d or da <> d ) ;
suppose A12: da = d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((s +* (Start-At (((IC s) + k),SCM))) . da) + ((s +* (Start-At (((IC s) + k),SCM))) . db) by A10, AMI_3:9
.= (s . da) + ((s +* (Start-At (((IC s) + k),SCM))) . db) by AMI_5:80
.= (s . da) + (s . db) by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A10, A12, AMI_3:9
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
suppose A13: da <> d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A10, AMI_3:9
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A10, A13, AMI_3:9
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
end;
end;
A14: IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) by A1, A10, AMI_3:9;
( IncAddr ((CurInstr ((ProgramPart s),s)),k) = CurInstr ((ProgramPart s),s) & IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = succ (IC s) ) by A10, AMI_3:9, COMPOS_1:92;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) by A2, A14, A11, AMI_5:26; :: 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)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then consider da, db being Data-Location such that
A15: CurInstr ((ProgramPart s),s) = SubFrom (da,db) by AMI_5:49;
A16: now
let d be Data-Location ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
per cases ( da = d or da <> d ) ;
suppose A17: da = d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((s +* (Start-At (((IC s) + k),SCM))) . da) - ((s +* (Start-At (((IC s) + k),SCM))) . db) by A15, AMI_3:10
.= (s . da) - ((s +* (Start-At (((IC s) + k),SCM))) . db) by AMI_5:80
.= (s . da) - (s . db) by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A15, A17, AMI_3:10
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
suppose A18: da <> d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A15, AMI_3:10
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A15, A18, AMI_3:10
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
end;
end;
A19: IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) by A1, A15, AMI_3:10;
( IncAddr ((CurInstr ((ProgramPart s),s)),k) = CurInstr ((ProgramPart s),s) & IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = succ (IC s) ) by A15, AMI_3:10, COMPOS_1:92;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) by A2, A19, A16, AMI_5:26; :: 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)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then consider da, db being Data-Location such that
A20: CurInstr ((ProgramPart s),s) = MultBy (da,db) by AMI_5:50;
A21: now
let d be Data-Location ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
per cases ( da = d or da <> d ) ;
suppose A22: da = d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((s +* (Start-At (((IC s) + k),SCM))) . da) * ((s +* (Start-At (((IC s) + k),SCM))) . db) by A20, AMI_3:11
.= (s . da) * ((s +* (Start-At (((IC s) + k),SCM))) . db) by AMI_5:80
.= (s . da) * (s . db) by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A20, A22, AMI_3:11
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
suppose A23: da <> d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A20, AMI_3:11
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A20, A23, AMI_3:11
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
end;
end;
A24: IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) by A1, A20, AMI_3:11;
( IncAddr ((CurInstr ((ProgramPart s),s)),k) = CurInstr ((ProgramPart s),s) & IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = succ (IC s) ) by A20, AMI_3:11, COMPOS_1:92;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) by A2, A24, A21, AMI_5:26; :: 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)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then consider da, db being Data-Location such that
A25: CurInstr ((ProgramPart s),s) = Divide (da,db) by AMI_5:51;
A26: now
let d be Data-Location ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
per cases ( da <> db or da = db ) ;
suppose A27: da <> db ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hereby :: thesis: verum
per cases ( da = d or db = d or ( da <> d & db <> d ) ) ;
suppose A28: da = d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((s +* (Start-At (((IC s) + k),SCM))) . da) div ((s +* (Start-At (((IC s) + k),SCM))) . db) by A25, A27, AMI_3:12
.= (s . da) div ((s +* (Start-At (((IC s) + k),SCM))) . db) by AMI_5:80
.= (s . da) div (s . db) by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A25, A27, A28, AMI_3:12
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
suppose A29: db = d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((s +* (Start-At (((IC s) + k),SCM))) . da) mod ((s +* (Start-At (((IC s) + k),SCM))) . db) by A25, AMI_3:12
.= (s . da) mod ((s +* (Start-At (((IC s) + k),SCM))) . db) by AMI_5:80
.= (s . da) mod (s . db) by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A25, A29, AMI_3:12
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
suppose A30: ( da <> d & db <> d ) ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A25, AMI_3:12
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A25, A30, AMI_3:12
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
end;
end;
end;
suppose A31: da = db ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . b1 = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . b1
hereby :: thesis: verum
per cases ( da = d or da <> d ) ;
suppose A32: da = d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((s +* (Start-At (((IC s) + k),SCM))) . da) mod ((s +* (Start-At (((IC s) + k),SCM))) . da) by A25, A31, AMI_3:12
.= (s . da) mod ((s +* (Start-At (((IC s) + k),SCM))) . da) by AMI_5:80
.= (s . da) mod (s . da) by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A25, A31, A32, AMI_3:12
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
suppose A33: da <> d ; :: thesis: (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d
hence (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A25, A31, AMI_3:12
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A25, A31, A33, AMI_3:12
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) . d by AMI_5:80 ;
:: thesis: verum
end;
end;
end;
end;
end;
end;
A34: IC (Exec ((CurInstr ((ProgramPart s),s)),(s +* (Start-At (((IC s) + k),SCM))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((succ (IC s)) + k),SCM))) by A1, A25, AMI_3:12;
( IncAddr ((CurInstr ((ProgramPart s),s)),k) = CurInstr ((ProgramPart s),s) & IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = succ (IC s) ) by A25, AMI_3:12, COMPOS_1:92;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) by A2, A34, A26, AMI_5:26; :: 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)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then consider loc being Element of NAT such that
A35: CurInstr ((ProgramPart s),s) = SCM-goto loc by AMI_5:52;
A36: IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = loc by A35, AMI_3:13;
A37: now
let d be Element of NAT ; :: thesis: (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . 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))) . d by COMPOS_1:20 ; :: thesis: verum
end;
A38: IncAddr ((CurInstr ((ProgramPart s),s)),k) = SCM-goto (loc + k) by A35, Th10;
A39: now
let d be Data-Location ; :: thesis: (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A38, AMI_3:13
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A35, AMI_3:13
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d by AMI_5:80 ; :: thesis: verum
end;
IC (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) = loc + k by A38, AMI_3:13
.= IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) by A36, FUNCT_4:121 ;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) by A39, A37, AMI_5:26; :: 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)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then consider loc being Element of NAT , da being Data-Location such that
A40: CurInstr ((ProgramPart s),s) = da =0_goto loc by AMI_5:53;
A41: IncAddr ((CurInstr ((ProgramPart s),s)),k) = da =0_goto (loc + k) by A40, Th11;
now
per cases ( s . da = 0 or s . da <> 0 ) ;
suppose A42: s . da = 0 ; :: thesis: Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))
A43: now
let d be Data-Location ; :: thesis: (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A41, AMI_3:14
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A40, AMI_3:14
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d by AMI_5:80 ; :: thesis: verum
end;
A44: now
let d be Element of NAT ; :: thesis: (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . 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))) . d by COMPOS_1:20 ; :: thesis: verum
end;
A45: IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = loc by A40, A42, AMI_3:14;
(s +* (Start-At (((IC s) + k),SCM))) . da = 0 by A42, AMI_5:80;
then IC (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) = loc + k by A41, AMI_3:14
.= IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) by A45, FUNCT_4:121 ;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM)) by A43, A44, AMI_5:26; :: thesis: verum
end;
suppose A46: s . da <> 0 ; :: thesis: Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))
A47: now
let d be Element of NAT ; :: thesis: (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . 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))) . d by COMPOS_1:20 ; :: thesis: verum
end;
A48: now
let d be Data-Location ; :: thesis: (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by A41, AMI_3:14
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A40, AMI_3:14
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d by AMI_5:80 ; :: thesis: verum
end;
( (s +* (Start-At (((IC s) + k),SCM))) . da <> 0 & IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = succ (IC s) ) by A40, A46, AMI_3:14, AMI_5:80;
then IC (Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) by A1, A41, AMI_3:14;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM)) by A48, A47, AMI_5:26; :: thesis: verum
end;
end;
end;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) ; :: thesis: verum
end;
suppose InsCode (CurInstr ((ProgramPart s),s)) = 8 ; :: thesis: Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM))
then consider loc being Element of NAT , da being Data-Location such that
A49: CurInstr ((ProgramPart s),s) = da >0_goto loc by AMI_5:54;
now
per cases ( s . da > 0 or s . da <= 0 ) ;
suppose A50: s . da > 0 ; :: thesis: Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))
A51: now
let d be Data-Location ; :: thesis: (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by AMI_3:15
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A49, AMI_3:15
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d by AMI_5:80 ; :: thesis: verum
end;
A52: now
let d be Element of NAT ; :: thesis: (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . 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))) . d by COMPOS_1:20 ; :: thesis: verum
end;
A53: IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = loc by A49, A50, AMI_3:15;
(s +* (Start-At (((IC s) + k),SCM))) . da > 0 by A50, AMI_5:80;
then IC (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) = loc + k by AMI_3:15
.= IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) by A53, FUNCT_4:121 ;
hence Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM)) by A51, A52, AMI_5:26; :: thesis: verum
end;
suppose A54: s . da <= 0 ; :: thesis: Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))
A55: now
let d be Element of NAT ; :: thesis: (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . 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))) . d by COMPOS_1:20 ; :: thesis: verum
end;
A56: now
let d be Data-Location ; :: thesis: (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d
thus (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) . d = (s +* (Start-At (((IC s) + k),SCM))) . d by AMI_3:15
.= s . d by AMI_5:80
.= (Exec ((CurInstr ((ProgramPart s),s)),s)) . d by A49, AMI_3:15
.= ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) . d by AMI_5:80 ; :: thesis: verum
end;
( (s +* (Start-At (((IC s) + k),SCM))) . da <= 0 & IC (Exec ((CurInstr ((ProgramPart s),s)),s)) = succ (IC s) ) by A49, A54, AMI_3:15, AMI_5:80;
then IC (Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM))))) = IC ((Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM))) by A1, AMI_3:15;
hence Exec ((da >0_goto (loc + k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Exec ((CurInstr ((ProgramPart s),s)),s)) +* (Start-At (((IC (Exec ((CurInstr ((ProgramPart s),s)),s))) + k),SCM)) by A56, A55, AMI_5:26; :: thesis: verum
end;
end;
end;
hence Exec ((IncAddr ((CurInstr ((ProgramPart s),s)),k)),(s +* (Start-At (((IC s) + k),SCM)))) = (Following ((ProgramPart s),s)) +* (Start-At (((IC (Following ((ProgramPart s),s))) + k),SCM)) by A49, Th12; :: thesis: verum
end;
end;