let INS be Instruction of SCM+FSA; :: 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 R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (b1,k))), IncIC ((Exec ((IncAddr (INS,j)),b1)),k))
let s be State of SCM+FSA; :: thesis: R48( the U1 of SCM+FSA, 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 = 12 by SCMFSA_2:16;
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 or InsCode INS = 8 or InsCode INS = 9 or InsCode INS = 10 or InsCode INS = 11 or InsCode INS = 12 ) ;
suppose InsCode INS = 0 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then A2: INS = halt SCM+FSA by SCMFSA_2:95;
then A3: IncAddr (INS,j) = halt SCM+FSA by COMPOS_0:4;
Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = Exec (INS,(IncIC (s,k))) by A2, COMPOS_0:4
.= IncIC (s,k) by A2, EXTPRO_1:def 3
.= IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A3, EXTPRO_1:def 3 ;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) ; :: thesis: verum
end;
suppose InsCode INS = 1 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A4: INS = da := db by SCMFSA_2:30;
A5: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A4, COMPOS_0:4
.= (IncIC (s,k)) . f by A4, SCMFSA_2:63
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A4, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . f by A4, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-Location; :: 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 A6: 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 A4, COMPOS_0:4
.= (IncIC (s,k)) . db by A4, A6, SCMFSA_2:63
.= s . db by SCMFSA_3:3
.= (Exec (INS,s)) . d by A4, A6, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . d by A4, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
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 A4, COMPOS_0:4
.= (IncIC (s,k)) . d by A4, A7, SCMFSA_2:63
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A4, A7, SCMFSA_2:63
.= (Exec ((IncAddr (INS,j)),s)) . d by A4, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
end;
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A5, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 2 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A8: INS = AddTo (da,db) by SCMFSA_2:31;
A9: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A8, COMPOS_0:4
.= (IncIC (s,k)) . f by A8, SCMFSA_2:64
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A8, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . f by A8, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-Location; :: 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 A8, COMPOS_0:4
.= ((IncIC (s,k)) . da) + ((IncIC (s,k)) . db) by A10, A8, SCMFSA_2:64
.= (s . da) + ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) + (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A8, A10, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . d by A8, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: 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 A8, COMPOS_0:4
.= (IncIC (s,k)) . d by A8, A11, SCMFSA_2:64
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A8, A11, SCMFSA_2:64
.= (Exec ((IncAddr (INS,j)),s)) . d by A8, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
end;
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A9, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 3 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A12: INS = SubFrom (da,db) by SCMFSA_2:32;
A13: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A12, COMPOS_0:4
.= (IncIC (s,k)) . f by A12, SCMFSA_2:65
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A12, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . f by A12, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-Location; :: 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 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)) . da) - ((IncIC (s,k)) . db) by A14, A12, SCMFSA_2:65
.= (s . da) - ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) - (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A12, A14, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
suppose A15: 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, A15, SCMFSA_2:65
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A12, A15, SCMFSA_2:65
.= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
end;
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A13, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 4 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A16: INS = MultBy (da,db) by SCMFSA_2:33;
A17: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A16, COMPOS_0:4
.= (IncIC (s,k)) . f by A16, SCMFSA_2:66
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A16, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . f by A16, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-Location; :: 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 A18: 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 A16, COMPOS_0:4
.= ((IncIC (s,k)) . da) * ((IncIC (s,k)) . db) by A18, A16, SCMFSA_2:66
.= (s . da) * ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) * (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A16, A18, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
suppose A19: 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 A16, COMPOS_0:4
.= (IncIC (s,k)) . d by A16, A19, SCMFSA_2:66
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A16, A19, SCMFSA_2:66
.= (Exec ((IncAddr (INS,j)),s)) . d by A16, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
end;
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A17, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 5 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da, db being Int-Location such that
A20: INS = Divide (da,db) by SCMFSA_2:34;
A21: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A20, COMPOS_0:4
.= (IncIC (s,k)) . f by A20, SCMFSA_2:67
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A20, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . f by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-Location; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
per cases ( da <> db or da = db ) ;
suppose A22: da <> db ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
hereby :: thesis: verum
per cases ( da = d or db = d or ( da <> d & db <> d ) ) ;
suppose A23: 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 A20, COMPOS_0:4
.= ((IncIC (s,k)) . da) div ((IncIC (s,k)) . db) by A22, A23, A20, SCMFSA_2:67
.= (s . da) div ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) div (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A22, A23, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
suppose A24: 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 A20, COMPOS_0:4
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A24, A20, SCMFSA_2:67
.= (s . da) mod ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) mod (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A24, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
suppose A25: ( 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 A20, COMPOS_0:4
.= (IncIC (s,k)) . d by A20, A25, SCMFSA_2:67
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A25, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
end;
end;
end;
suppose A26: da = db ; :: 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 A27: 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 A20, COMPOS_0:4
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A26, A27, A20, SCMFSA_2:67
.= (s . da) mod ((IncIC (s,k)) . db) by SCMFSA_3:3
.= (s . da) mod (s . db) by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A26, A27, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
suppose A28: 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 A20, COMPOS_0:4
.= (IncIC (s,k)) . d by A20, A26, A28, SCMFSA_2:67
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A20, A26, A28, SCMFSA_2:67
.= (Exec ((IncAddr (INS,j)),s)) . d by A20, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
end;
end;
end;
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A21, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 6 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider loc being Nat such that
A29: INS = goto loc by SCMFSA_2:35;
A30: IncAddr (INS,(j + k)) = goto (loc + (j + k)) by A29, Th1;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
A31: IncAddr (INS,jj) = goto (loc + jj) by A29, Th1;
A32: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A30, SCMFSA_2:69
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A31, SCMFSA_2:69
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-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 A30, SCMFSA_2:69
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A31, SCMFSA_2:69
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A32, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 7 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider loc being Nat, da being Int-Location such that
A33: INS = da =0_goto loc by SCMFSA_2:36;
A34: IncAddr (INS,(j + k)) = da =0_goto (loc + (j + k)) by A33, Th2;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
A35: IncAddr (INS,jj) = da =0_goto (loc + jj) by A33, Th2;
A36: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A34, SCMFSA_2:70
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A35, SCMFSA_2:70
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-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 A34, SCMFSA_2:70
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A35, SCMFSA_2:70
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A1, A36, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 8 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider loc being Nat, da being Int-Location such that
A37: INS = da >0_goto loc by SCMFSA_2:37;
A38: IncAddr (INS,(j + k)) = da >0_goto (loc + (j + k)) by A37, Th3;
reconsider jj = j as Element of NAT by ORDINAL1:def 12;
A39: IncAddr (INS,jj) = da >0_goto (loc + jj) by A37, Th3;
A40: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC (s,k)) . f by A38, SCMFSA_2:71
.= s . f by SCMFSA_3:4
.= (Exec ((IncAddr (INS,j)),s)) . f by A39, SCMFSA_2:71
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-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 A38, SCMFSA_2:71
.= s . d by SCMFSA_3:3
.= (Exec ((IncAddr (INS,j)),s)) . d by A39, SCMFSA_2:71
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A40, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 9 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider db, da being Int-Location, f being FinSeq-Location such that
A41: INS = da := (f,db) by SCMFSA_2:38;
A42: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A41, COMPOS_0:4
.= (IncIC (s,k)) . f by A41, SCMFSA_2:72
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A41, SCMFSA_2:72
.= (Exec ((IncAddr (INS,j)),s)) . f by A41, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-Location; :: 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 A43: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
consider m being Nat such that
A44: m = |.(s . db).| and
A45: (Exec (INS,s)) . da = (s . f) /. m by A41, SCMFSA_2:72;
A46: ex m1 being Nat st
( m1 = |.((IncIC (s,k)) . db).| & (Exec (INS,(IncIC (s,k)))) . da = ((IncIC (s,k)) . f) /. m1 ) by A41, SCMFSA_2:72;
A47: (IncIC (s,k)) . db = s . db by SCMFSA_3:3;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A41, COMPOS_0:4
.= (s . f) /. m by A44, A46, A43, A47, SCMFSA_3:4
.= (IncIC ((Exec (INS,s)),k)) . d by A45, A43, SCMFSA_3:3
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by A41, COMPOS_0:4 ; :: thesis: verum
end;
suppose A48: 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 A41, COMPOS_0:4
.= (IncIC (s,k)) . d by A41, A48, SCMFSA_2:72
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A41, A48, SCMFSA_2:72
.= (Exec ((IncAddr (INS,j)),s)) . d by A41, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
end;
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A42, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 10 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider db, da being Int-Location, f being FinSeq-Location such that
A49: INS = (f,db) := da by SCMFSA_2:39;
A50: now :: thesis: for g being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g
let g be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
consider m being Nat such that
A51: m = |.(s . db).| and
A52: (Exec (INS,s)) . f = (s . f) +* (m,(s . da)) by A49, SCMFSA_2:73;
A53: ex m1 being Nat st
( m1 = |.((IncIC (s,k)) . db).| & (Exec (INS,(IncIC (s,k)))) . f = ((IncIC (s,k)) . f) +* (m1,((IncIC (s,k)) . da)) ) by A49, SCMFSA_2:73;
per cases ( f = g or f <> g ) ;
suppose A54: f = g ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A55: ( (IncIC (s,k)) . f = s . f & (IncIC (s,k)) . db = s . db ) by SCMFSA_3:3, SCMFSA_3:4;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A49, COMPOS_0:4
.= (s . f) +* (m,(s . da)) by A51, A53, A54, A55, SCMFSA_3:3
.= (IncIC ((Exec (INS,s)),k)) . g by A52, A54, SCMFSA_3:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A49, COMPOS_0:4 ; :: thesis: verum
end;
suppose A56: f <> g ; :: 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)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A49, COMPOS_0:4
.= (IncIC (s,k)) . g by A49, A56, SCMFSA_2:73
.= s . g by SCMFSA_3:4
.= (Exec (INS,s)) . g by A49, A56, SCMFSA_2:73
.= (Exec ((IncAddr (INS,j)),s)) . g by A49, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:4 ; :: thesis: verum
end;
end;
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-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 = (Exec (INS,(IncIC (s,k)))) . d by A49, COMPOS_0:4
.= (IncIC (s,k)) . d by A49, SCMFSA_2:73
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A49, SCMFSA_2:73
.= (Exec ((IncAddr (INS,j)),s)) . d by A49, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A50, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 11 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da being Int-Location, f being FinSeq-Location such that
A57: INS = da :=len f by SCMFSA_2:40;
A58: now :: thesis: for f being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
let f be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . f = (Exec (INS,(IncIC (s,k)))) . f by A57, COMPOS_0:4
.= (IncIC (s,k)) . f by A57, SCMFSA_2:74
.= s . f by SCMFSA_3:4
.= (Exec (INS,s)) . f by A57, SCMFSA_2:74
.= (Exec ((IncAddr (INS,j)),s)) . f by A57, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:4 ; :: thesis: verum
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-Location; :: 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 A59: 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 A57, COMPOS_0:4
.= len ((IncIC (s,k)) . f) by A59, A57, SCMFSA_2:74
.= len (s . f) by SCMFSA_3:4
.= (Exec (INS,s)) . d by A57, A59, SCMFSA_2:74
.= (IncIC ((Exec (INS,s)),k)) . d by SCMFSA_3:3
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by A57, COMPOS_0:4 ; :: thesis: verum
end;
suppose A60: 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 A57, COMPOS_0:4
.= (IncIC (s,k)) . d by A57, A60, SCMFSA_2:74
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A57, A60, SCMFSA_2:74
.= (Exec ((IncAddr (INS,j)),s)) . d by A57, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
end;
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A58, A1, SCMFSA_2:104; :: thesis: verum
end;
suppose InsCode INS = 12 ; :: thesis: R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da being Int-Location, f being FinSeq-Location such that
A61: INS = f :=<0,...,0> da by SCMFSA_2:41;
A62: now :: thesis: for g being FinSeq-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g
let g be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A63: ( ex m being Nat st
( m = |.(s . da).| & (Exec (INS,s)) . f = m |-> 0 ) & ex m being Nat st
( m = |.((IncIC (s,k)) . da).| & (Exec (INS,(IncIC (s,k)))) . f = m |-> 0 ) ) by A61, SCMFSA_2:75;
per cases ( f = g or f <> g ) ;
suppose A64: f = g ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A65: (IncIC (s,k)) . da = s . da by SCMFSA_3:3;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A61, COMPOS_0:4
.= (IncIC ((Exec (INS,s)),k)) . g by A63, A64, A65, SCMFSA_3:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A61, COMPOS_0:4 ; :: thesis: verum
end;
suppose A66: f <> g ; :: 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)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A61, COMPOS_0:4
.= (IncIC (s,k)) . g by A61, A66, SCMFSA_2:75
.= s . g by SCMFSA_3:4
.= (Exec (INS,s)) . g by A61, A66, SCMFSA_2:75
.= (Exec ((IncAddr (INS,j)),s)) . g by A61, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:4 ; :: thesis: verum
end;
end;
end;
now :: thesis: for d being Int-Location holds (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d
let d be Int-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 = (Exec (INS,(IncIC (s,k)))) . d by A61, COMPOS_0:4
.= (IncIC (s,k)) . d by A61, SCMFSA_2:75
.= s . d by SCMFSA_3:3
.= (Exec (INS,s)) . d by A61, SCMFSA_2:75
.= (Exec ((IncAddr (INS,j)),s)) . d by A61, COMPOS_0:4
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:3 ; :: thesis: verum
end;
hence R48( the U1 of SCM+FSA, Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))), IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A62, A1, SCMFSA_2:104; :: thesis: verum
end;
end;