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 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 AMI_1:def 8;
X: IncAddr (CurInstr (ProgramPart s),s),k = CurInstr (ProgramPart s),s by A3, AMISTD_2:30;
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 A3, X, AMI_5:37
.= (Following (ProgramPart s),s) +* (Start-At ((IC (Following (ProgramPart s),s)) + k),SCM ) by A4, AMI_1:def 8 ; :: 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, AMISTD_2:29, AMI_3:8;
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, AMISTD_2:29, AMI_3:9;
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, AMISTD_2:29, AMI_3:10;
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, AMISTD_2:29, AMI_3:11;
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, AMISTD_2:29, AMI_3:12;
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;