let INS be Instruction of (SCM R); :: according to AMISTD_5:def 2 :: thesis: INS is relocable
let j, k be Nat; :: according to AMISTD_5:def 1 :: thesis: for b1 being set holds Exec ((IncAddr (INS,(j + k))),(IncIC (b1,k))) = IncIC ((Exec ((IncAddr (INS,j)),b1)),k)
reconsider k = k as Element of NAT by ORDINAL1:def 12;
let s be State of (SCM R); :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
A1: IC (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) = (IC (Exec ((IncAddr (INS,j)),s))) + k by MEMSTR_0:53
.= IC (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) by AMISTD_2:def 3 ;
not not InsCode INS = 0 & ... & not InsCode INS = 7 by SCMRING3:39;
per cases then ( 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 ) ;
suppose InsCode INS = 0 ; :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
then A2: INS = halt (SCM R) by SCMRING3:12;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC (s,k) by A2, EXTPRO_1:def 3
.= IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A2, EXTPRO_1:def 3 ;
hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) ; :: thesis: verum
end;
suppose InsCode INS = 1 ; :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
then consider da, db being Data-Location of R such that
A3: INS = da := db by SCMRING3:13;
now :: thesis: for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Data-Location of R; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
per cases ( da = d or da <> d ) ;
suppose A4: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A3, COMPOS_0:4
.= (IncIC (s,k)) . db by A3, A4, SCMRING2:11
.= s . db by Th5
.= (Exec (INS,s)) . d by A3, A4, SCMRING2:11
.= (Exec ((IncAddr (INS,j)),s)) . d by A3, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
suppose A5: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A3, COMPOS_0:4
.= (IncIC (s,k)) . d by A3, A5, SCMRING2:11
.= s . d by Th5
.= (Exec (INS,s)) . d by A3, A5, SCMRING2:11
.= (Exec ((IncAddr (INS,j)),s)) . d by A3, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
end;
end;
hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; :: thesis: verum
end;
suppose InsCode INS = 2 ; :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
then consider da, db being Data-Location of R such that
A6: INS = AddTo (da,db) by SCMRING3:14;
now :: thesis: for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Data-Location of R; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
per cases ( da = d or da <> d ) ;
suppose A7: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A6, COMPOS_0:4
.= ((IncIC (s,k)) . da) + ((IncIC (s,k)) . db) by A7, A6, SCMRING2:12
.= (s . da) + ((IncIC (s,k)) . db) by Th5
.= (s . da) + (s . db) by Th5
.= (Exec (INS,s)) . d by A6, A7, SCMRING2:12
.= (Exec ((IncAddr (INS,j)),s)) . d by A6, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
suppose A8: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A6, COMPOS_0:4
.= (IncIC (s,k)) . d by A6, A8, SCMRING2:12
.= s . d by Th5
.= (Exec (INS,s)) . d by A6, A8, SCMRING2:12
.= (Exec ((IncAddr (INS,j)),s)) . d by A6, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
end;
end;
hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; :: thesis: verum
end;
suppose InsCode INS = 3 ; :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
then consider da, db being Data-Location of R such that
A9: INS = SubFrom (da,db) by SCMRING3:15;
now :: thesis: for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Data-Location of R; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
per cases ( da = d or da <> d ) ;
suppose A10: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A9, COMPOS_0:4
.= ((IncIC (s,k)) . da) - ((IncIC (s,k)) . db) by A10, A9, SCMRING2:13
.= (s . da) - ((IncIC (s,k)) . db) by Th5
.= (s . da) - (s . db) by Th5
.= (Exec (INS,s)) . d by A9, A10, SCMRING2:13
.= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
suppose A11: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A9, COMPOS_0:4
.= (IncIC (s,k)) . d by A9, A11, SCMRING2:13
.= s . d by Th5
.= (Exec (INS,s)) . d by A9, A11, SCMRING2:13
.= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
end;
end;
hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; :: thesis: verum
end;
suppose InsCode INS = 4 ; :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
then consider da, db being Data-Location of R such that
A12: INS = MultBy (da,db) by SCMRING3:16;
now :: thesis: for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Data-Location of R; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
per cases ( da = d or da <> d ) ;
suppose A13: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A12, COMPOS_0:4
.= ((IncIC (s,k)) . da) * ((IncIC (s,k)) . db) by A13, A12, SCMRING2:14
.= (s . da) * ((IncIC (s,k)) . db) by Th5
.= (s . da) * (s . db) by Th5
.= (Exec (INS,s)) . d by A12, A13, SCMRING2:14
.= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
suppose A14: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A12, COMPOS_0:4
.= (IncIC (s,k)) . d by A12, A14, SCMRING2:14
.= s . d by Th5
.= (Exec (INS,s)) . d by A12, A14, SCMRING2:14
.= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
end;
end;
hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; :: thesis: verum
end;
suppose InsCode INS = 5 ; :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
then consider da being Data-Location of R, r being Element of R such that
A15: INS = da := r by SCMRING3:17;
now :: thesis: for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Data-Location of R; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
per cases ( da = d or da <> d ) ;
suppose A16: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A15, COMPOS_0:4
.= r by A16, A15, SCMRING2:17
.= (Exec (INS,s)) . d by A15, A16, SCMRING2:17
.= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
suppose A17: da <> d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A15, COMPOS_0:4
.= (IncIC (s,k)) . d by A15, A17, SCMRING2:17
.= s . d by Th5
.= (Exec (INS,s)) . d by A15, A17, SCMRING2:17
.= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
end;
end;
hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; :: thesis: verum
end;
suppose InsCode INS = 6 ; :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
then consider loc being Nat such that
A18: INS = goto (loc,R) by SCMRING3:18;
A19: IncAddr (INS,(j + k)) = goto ((loc + (j + k)),R) by A18, SCMRING3:37;
A20: IncAddr (INS,j) = goto ((loc + j),R) by A18, SCMRING3:37;
now :: thesis: for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Data-Location of R; :: 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 A19, SCMRING2:15
.= s . d by Th5
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, SCMRING2:15
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; :: thesis: verum
end;
suppose InsCode INS = 7 ; :: thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k)
then consider da being Data-Location of R, loc being Nat such that
A21: INS = da =0_goto loc by SCMRING3:19;
A22: IncAddr (INS,(j + k)) = da =0_goto (loc + (j + k)) by A21, SCMRING3:38;
A23: IncAddr (INS,j) = da =0_goto (loc + j) by A21, SCMRING3:38;
now :: thesis: for d being Data-Location of R holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Data-Location of R; :: 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 A22, SCMRING2:16
.= s . d by Th5
.= (Exec ((IncAddr (INS,j)),s)) . d by A23, SCMRING2:16
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; :: thesis: verum
end;
hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, Th6; :: thesis: verum
end;
end;