let INS be Instruction of SCM; :: according to AMISTD_5:def 2 :: thesis: INS is relocable
let j, k be Nat; :: according to AMISTD_5:def 1 :: thesis: for b₁ being set holds NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (b₁,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),b₁)),k))
reconsider k = k as Element of NAT by ORDINAL1:def 13;
let s be State of SCM; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))
A1: IC (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) = (IC (Exec ((IncAddr (INS,j)),s))) + k by COMPOS_1:54
.= IC (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) by AMISTD_2:def 18 ;

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 InsCode INS = 0 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then A3: INS = halt SCM by AMI_5:46;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = Exec (INS,(IncIC (s,k))) by A3, COMPOS_1:93
.= IncIC (s,k) by EXTPRO_1:def 3, A3
.= IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A3, EXTPRO_1:def 3 ;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) ; :: thesis: verum

end;

suppose InsCode INS = 1 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then consider da, db being Data-Location such that
A4: INS = da := db by AMI_5:47;

now

let d be Data-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

per cases ( da = d or da <> d ) ;

suppose A5: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A4, COMPOS_1:92
.= (IncIC (s,k)) . db by A4, A5, AMI_3:8
.= s . db by AMI_5:80
.= (Exec (INS,s)) . d by A4, A5, AMI_3:8
.= (Exec ((IncAddr (INS,j)),s)) . d by A4, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

suppose A6: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A4, COMPOS_1:92
.= (IncIC (s,k)) . d by A4, A6, AMI_3:8
.= s . d by AMI_5:80
.= (Exec (INS,s)) . d by A4, A6, AMI_3:8
.= (Exec ((IncAddr (INS,j)),s)) . d by A4, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

end;

end;

hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by AMI_5:96, A1; :: thesis: verum

end;

suppose InsCode INS = 2 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then consider da, db being Data-Location such that
A7: INS = AddTo (da,db) by AMI_5:48;

now

let d be Data-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

per cases ( da = d or da <> d ) ;

suppose A8: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A7, COMPOS_1:92
.= ((IncIC (s,k)) . da) + ((IncIC (s,k)) . db) by A8, A7, AMI_3:9
.= (s . da) + ((IncIC (s,k)) . db) by AMI_5:80
.= (s . da) + (s . db) by AMI_5:80
.= (Exec (INS,s)) . d by A7, A8, AMI_3:9
.= (Exec ((IncAddr (INS,j)),s)) . d by A7, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

suppose A9: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A7, COMPOS_1:92
.= (IncIC (s,k)) . d by A7, A9, AMI_3:9
.= s . d by AMI_5:80
.= (Exec (INS,s)) . d by A7, A9, AMI_3:9
.= (Exec ((IncAddr (INS,j)),s)) . d by A7, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

end;

end;

hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by AMI_5:96, A1; :: thesis: verum

end;

suppose InsCode INS = 3 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then consider da, db being Data-Location such that
A10: INS = SubFrom (da,db) by AMI_5:49;

now

let d be Data-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

per cases ( da = d or da <> d ) ;

suppose A11: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A10, COMPOS_1:92
.= ((IncIC (s,k)) . da) - ((IncIC (s,k)) . db) by A11, A10, AMI_3:10
.= (s . da) - ((IncIC (s,k)) . db) by AMI_5:80
.= (s . da) - (s . db) by AMI_5:80
.= (Exec (INS,s)) . d by A10, A11, AMI_3:10
.= (Exec ((IncAddr (INS,j)),s)) . d by A10, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

suppose A12: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A10, COMPOS_1:92
.= (IncIC (s,k)) . d by A10, A12, AMI_3:10
.= s . d by AMI_5:80
.= (Exec (INS,s)) . d by A10, A12, AMI_3:10
.= (Exec ((IncAddr (INS,j)),s)) . d by A10, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

end;

end;

hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by AMI_5:96, A1; :: thesis: verum

end;

suppose InsCode INS = 4 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then consider da, db being Data-Location such that
A13: INS = MultBy (da,db) by AMI_5:50;

now

let d be Data-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

per cases ( da = d or da <> d ) ;

suppose A14: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A13, COMPOS_1:92
.= ((IncIC (s,k)) . da) * ((IncIC (s,k)) . db) by A14, A13, AMI_3:11
.= (s . da) * ((IncIC (s,k)) . db) by AMI_5:80
.= (s . da) * (s . db) by AMI_5:80
.= (Exec (INS,s)) . d by A13, A14, AMI_3:11
.= (Exec ((IncAddr (INS,j)),s)) . d by A13, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

suppose A15: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A13, COMPOS_1:92
.= (IncIC (s,k)) . d by A13, A15, AMI_3:11
.= s . d by AMI_5:80
.= (Exec (INS,s)) . d by A13, A15, AMI_3:11
.= (Exec ((IncAddr (INS,j)),s)) . d by A13, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

end;

end;

hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by AMI_5:96, A1; :: thesis: verum

end;

suppose InsCode INS = 5 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then consider da, db being Data-Location such that
A16: INS = Divide (da,db) by AMI_5:51;

now

let d be Data-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

per cases ( da <> db or da = db ) ;

suppose A17: da <> db ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

hereby :: thesis: verum

per cases ( da = d or db = d or ( da <> d & db <> d ) ) ;

suppose A18: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A16, COMPOS_1:92
.= ((IncIC (s,k)) . da) div ((IncIC (s,k)) . db) by A17, A18, A16, AMI_3:12
.= (s . da) div ((IncIC (s,k)) . db) by AMI_5:80
.= (s . da) div (s . db) by AMI_5:80
.= (Exec (INS,s)) . d by A16, A17, A18, AMI_3:12
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

suppose A19: db = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A16, COMPOS_1:92
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A19, A16, AMI_3:12
.= (s . da) mod ((IncIC (s,k)) . db) by AMI_5:80
.= (s . da) mod (s . db) by AMI_5:80
.= (Exec (INS,s)) . d by A16, A19, AMI_3:12
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

suppose A20: ( da <> d & db <> d ) ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A16, COMPOS_1:92
.= (IncIC (s,k)) . d by A16, A20, AMI_3:12
.= s . d by AMI_5:80
.= (Exec (INS,s)) . d by A16, A20, AMI_3:12
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

end;

end;

end;

suppose A21: da = db ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

per cases ( da = d or da <> d ) ;

suppose A22: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A16, COMPOS_1:92
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A21, A22, A16, AMI_3:12
.= (s . da) mod ((IncIC (s,k)) . db) by AMI_5:80
.= (s . da) mod (s . db) by AMI_5:80
.= (Exec (INS,s)) . d by A16, A21, A22, AMI_3:12
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

suppose A23: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b₁ = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b₁

thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A16, COMPOS_1:92
.= (IncIC (s,k)) . d by A16, A21, A23, AMI_3:12
.= s . d by AMI_5:80
.= (Exec (INS,s)) . d by A16, A21, A23, AMI_3:12
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

end;

end;

end;

end;

hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by AMI_5:96, A1; :: thesis: verum

end;

suppose InsCode INS = 6 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then consider loc being Element of NAT such that
A24: INS = SCM-goto loc by AMI_5:52;
A25: IncAddr (INS,(j + k)) = SCM-goto (loc + (j + k)) by A24, Th1;
A26: IncAddr (INS,j) = SCM-goto (loc + j) by A24, Th1;

now

let d be Data-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A25, AMI_3:13
.= s . d by AMI_5:80
.= (Exec ((IncAddr (INS,j)),s)) . d by A26, AMI_3:13
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by AMI_5:96, A1; :: thesis: verum

end;

suppose InsCode INS = 7 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then consider loc being Element of NAT , da being Data-Location such that
A27: INS = da =0_goto loc by AMI_5:53;
A28: IncAddr (INS,(j + k)) = da =0_goto (loc + (j + k)) by A27, Th2;
A29: IncAddr (INS,j) = da =0_goto (loc + j) by A27, Th2;

now

let d be Data-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A28, AMI_3:14
.= s . d by AMI_5:80
.= (Exec ((IncAddr (INS,j)),s)) . d by A29, AMI_3:14
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A1, AMI_5:96; :: thesis: verum

end;

suppose InsCode INS = 8 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))

then consider loc being Element of NAT , da being Data-Location such that
A30: INS = da >0_goto loc by AMI_5:54;
A31: IncAddr (INS,(j + k)) = da >0_goto (loc + (j + k)) by A30, Th3;
A32: IncAddr (INS,j) = da >0_goto (loc + j) by A30, Th3;

now

let d be Data-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A31, AMI_3:15
.= s . d by AMI_5:80
.= (Exec ((IncAddr (INS,j)),s)) . d by A32, AMI_3:15
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:80 ; :: thesis: verum

end;

hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by AMI_5:96, A1; :: thesis: verum

end;

end;