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