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 NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (b1,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),b1)),k))
reconsider k = k as Element of NAT by ORDINAL1:def 13;
let s be State of SCM+FSA; :: 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 or InsCode INS = 9 or InsCode INS = 10 or InsCode INS = 11 or InsCode INS = 12 or InsCode INS = 13 ) by SCMFSA_2:35, NAT_1:38;
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+FSA by SCMFSA_2:122;
then A4: IncAddr (INS,j) = halt SCM+FSA by COMPOS_1:93;
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 A4, 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 Int-Location such that
A5: INS = da := db by SCMFSA_2:54;
A6: now
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 A5, COMPOS_1:92
.= (IncIC (s,k)) . f by A5, SCMFSA_2:89
.= s . f by SCMFSA_3:12
.= (Exec (INS,s)) . f by A5, SCMFSA_2:89
.= (Exec ((IncAddr (INS,j)),s)) . f by A5, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 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 A5, COMPOS_1:92
.= (IncIC (s,k)) . db by A5, A7, SCMFSA_2:89
.= s . db by SCMFSA_3:11
.= (Exec (INS,s)) . d by A5, A7, SCMFSA_2:89
.= (Exec ((IncAddr (INS,j)),s)) . d by A5, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: 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 A5, COMPOS_1:92
.= (IncIC (s,k)) . d by A5, A8, SCMFSA_2:89
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A5, A8, SCMFSA_2:89
.= (Exec ((IncAddr (INS,j)),s)) . d by A5, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
end;
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A6, SCMFSA_2:138, 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 Int-Location such that
A9: INS = AddTo (da,db) by SCMFSA_2:55;
A10: now
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 A9, COMPOS_1:92
.= (IncIC (s,k)) . f by A9, SCMFSA_2:90
.= s . f by SCMFSA_3:12
.= (Exec (INS,s)) . f by A9, SCMFSA_2:90
.= (Exec ((IncAddr (INS,j)),s)) . f by A9, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 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_1:92
.= ((IncIC (s,k)) . da) + ((IncIC (s,k)) . db) by A11, A9, SCMFSA_2:90
.= (s . da) + ((IncIC (s,k)) . db) by SCMFSA_3:11
.= (s . da) + (s . db) by SCMFSA_3:11
.= (Exec (INS,s)) . d by A9, A11, SCMFSA_2:90
.= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
suppose A12: 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_1:92
.= (IncIC (s,k)) . d by A9, A12, SCMFSA_2:90
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A9, A12, SCMFSA_2:90
.= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
end;
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A10, SCMFSA_2:138, 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 Int-Location such that
A13: INS = SubFrom (da,db) by SCMFSA_2:56;
A14: now
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 A13, COMPOS_1:92
.= (IncIC (s,k)) . f by A13, SCMFSA_2:91
.= s . f by SCMFSA_3:12
.= (Exec (INS,s)) . f by A13, SCMFSA_2:91
.= (Exec ((IncAddr (INS,j)),s)) . f by A13, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 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 A13, COMPOS_1:92
.= ((IncIC (s,k)) . da) - ((IncIC (s,k)) . db) by A15, A13, SCMFSA_2:91
.= (s . da) - ((IncIC (s,k)) . db) by SCMFSA_3:11
.= (s . da) - (s . db) by SCMFSA_3:11
.= (Exec (INS,s)) . d by A13, A15, SCMFSA_2:91
.= (Exec ((IncAddr (INS,j)),s)) . d by A13, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
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 A13, COMPOS_1:92
.= (IncIC (s,k)) . d by A13, A16, SCMFSA_2:91
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A13, A16, SCMFSA_2:91
.= (Exec ((IncAddr (INS,j)),s)) . d by A13, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
end;
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A14, SCMFSA_2:138, 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 Int-Location such that
A17: INS = MultBy (da,db) by SCMFSA_2:57;
A18: now
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 A17, COMPOS_1:92
.= (IncIC (s,k)) . f by A17, SCMFSA_2:92
.= s . f by SCMFSA_3:12
.= (Exec (INS,s)) . f by A17, SCMFSA_2:92
.= (Exec ((IncAddr (INS,j)),s)) . f by A17, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 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 A17, COMPOS_1:92
.= ((IncIC (s,k)) . da) * ((IncIC (s,k)) . db) by A19, A17, SCMFSA_2:92
.= (s . da) * ((IncIC (s,k)) . db) by SCMFSA_3:11
.= (s . da) * (s . db) by SCMFSA_3:11
.= (Exec (INS,s)) . d by A17, A19, SCMFSA_2:92
.= (Exec ((IncAddr (INS,j)),s)) . d by A17, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
suppose A20: 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 A17, COMPOS_1:92
.= (IncIC (s,k)) . d by A17, A20, SCMFSA_2:92
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A17, A20, SCMFSA_2:92
.= (Exec ((IncAddr (INS,j)),s)) . d by A17, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
end;
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A18, SCMFSA_2:138, 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 Int-Location such that
A21: INS = Divide (da,db) by SCMFSA_2:58;
A22: now
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 A21, COMPOS_1:92
.= (IncIC (s,k)) . f by A21, SCMFSA_2:93
.= s . f by SCMFSA_3:12
.= (Exec (INS,s)) . f by A21, SCMFSA_2:93
.= (Exec ((IncAddr (INS,j)),s)) . f by A21, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 A23: 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 A24: 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 A21, COMPOS_1:92
.= ((IncIC (s,k)) . da) div ((IncIC (s,k)) . db) by A23, A24, A21, SCMFSA_2:93
.= (s . da) div ((IncIC (s,k)) . db) by SCMFSA_3:11
.= (s . da) div (s . db) by SCMFSA_3:11
.= (Exec (INS,s)) . d by A21, A23, A24, SCMFSA_2:93
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
suppose A25: 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 A21, COMPOS_1:92
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A25, A21, SCMFSA_2:93
.= (s . da) mod ((IncIC (s,k)) . db) by SCMFSA_3:11
.= (s . da) mod (s . db) by SCMFSA_3:11
.= (Exec (INS,s)) . d by A21, A25, SCMFSA_2:93
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
suppose A26: ( 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 A21, COMPOS_1:92
.= (IncIC (s,k)) . d by A21, A26, SCMFSA_2:93
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A21, A26, SCMFSA_2:93
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
end;
end;
end;
suppose A27: 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 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 A21, COMPOS_1:92
.= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A27, A28, A21, SCMFSA_2:93
.= (s . da) mod ((IncIC (s,k)) . db) by SCMFSA_3:11
.= (s . da) mod (s . db) by SCMFSA_3:11
.= (Exec (INS,s)) . d by A21, A27, A28, SCMFSA_2:93
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
suppose A29: 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 A21, COMPOS_1:92
.= (IncIC (s,k)) . d by A21, A27, A29, SCMFSA_2:93
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A21, A27, A29, SCMFSA_2:93
.= (Exec ((IncAddr (INS,j)),s)) . d by A21, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: 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 A22, SCMFSA_2:138, 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
A30: INS = goto loc by SCMFSA_2:59;
A31: IncAddr (INS,(j + k)) = goto (loc + (j + k)) by A30, Th14;
reconsider jj = j as Element of NAT by ORDINAL1:def 13;
A32: IncAddr (INS,jj) = goto (loc + jj) by A30, Th14;
A33: now
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 A31, SCMFSA_2:95
.= s . f by SCMFSA_3:12
.= (Exec ((IncAddr (INS,j)),s)) . f by A32, SCMFSA_2:95
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 A31, SCMFSA_2:95
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,j)),s)) . d by A32, SCMFSA_2:95
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A33, SCMFSA_2:138, 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 Int-Location such that
A34: INS = da =0_goto loc by SCMFSA_2:60;
A35: IncAddr (INS,(j + k)) = da =0_goto (loc + (j + k)) by A34, Th15;
reconsider jj = j as Element of NAT by ORDINAL1:def 13;
A36: IncAddr (INS,jj) = da =0_goto (loc + jj) by A34, Th15;
A37: now
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 A35, SCMFSA_2:96
.= s . f by SCMFSA_3:12
.= (Exec ((IncAddr (INS,j)),s)) . f by A36, SCMFSA_2:96
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 A35, SCMFSA_2:96
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,j)),s)) . d by A36, SCMFSA_2:96
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A1, A37, SCMFSA_2:138; :: 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 Int-Location such that
A38: INS = da >0_goto loc by SCMFSA_2:61;
A39: IncAddr (INS,(j + k)) = da >0_goto (loc + (j + k)) by A38, Th16;
reconsider jj = j as Element of NAT by ORDINAL1:def 13;
A40: IncAddr (INS,jj) = da >0_goto (loc + jj) by A38, Th16;
A41: now
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 A39, SCMFSA_2:97
.= s . f by SCMFSA_3:12
.= (Exec ((IncAddr (INS,j)),s)) . f by A40, SCMFSA_2:97
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 A39, SCMFSA_2:97
.= s . d by SCMFSA_3:11
.= (Exec ((IncAddr (INS,j)),s)) . d by A40, SCMFSA_2:97
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A41, SCMFSA_2:138, A1; :: thesis: verum
end;
suppose InsCode INS = 9 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider db, da being Int-Location , f being FinSeq-Location such that
A42: INS = da := (f,db) by SCMFSA_2:62;
A43: now
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 A42, COMPOS_1:92
.= (IncIC (s,k)) . f by A42, SCMFSA_2:98
.= s . f by SCMFSA_3:12
.= (Exec (INS,s)) . f by A42, SCMFSA_2:98
.= (Exec ((IncAddr (INS,j)),s)) . f by A42, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 A44: da = d ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
consider m being Element of NAT such that
A45: m = abs (s . db) and
A46: (Exec (INS,s)) . da = (s . f) /. m by A42, SCMFSA_2:98;
A47: ex m1 being Element of NAT st
( m1 = abs ((IncIC (s,k)) . db) & (Exec (INS,(IncIC (s,k)))) . da = ((IncIC (s,k)) . f) /. m1 ) by A42, SCMFSA_2:98;
A48: (IncIC (s,k)) . db = s . db by SCMFSA_3:11;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A42, COMPOS_1:92
.= (s . f) /. m by A45, A47, A44, SCMFSA_3:12, A48
.= (IncIC ((Exec (INS,s)),k)) . d by A46, A44, SCMFSA_3:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by A42, COMPOS_1:92 ; :: thesis: verum
end;
suppose A49: 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 A42, COMPOS_1:92
.= (IncIC (s,k)) . d by A42, A49, SCMFSA_2:98
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A42, A49, SCMFSA_2:98
.= (Exec ((IncAddr (INS,j)),s)) . d by A42, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
end;
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A43, SCMFSA_2:138, A1; :: thesis: verum
end;
suppose InsCode INS = 10 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider db, da being Int-Location , f being FinSeq-Location such that
A50: INS = (f,db) := da by SCMFSA_2:63;
A51: now
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 Element of NAT such that
A52: m = abs (s . db) and
A53: (Exec (INS,s)) . f = (s . f) +* (m,(s . da)) by A50, SCMFSA_2:99;
A54: ex m1 being Element of NAT st
( m1 = abs ((IncIC (s,k)) . db) & (Exec (INS,(IncIC (s,k)))) . f = ((IncIC (s,k)) . f) +* (m1,((IncIC (s,k)) . da)) ) by A50, SCMFSA_2:99;
per cases ( f = g or f <> g ) ;
suppose A55: f = g ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A56: ( (IncIC (s,k)) . f = s . f & (IncIC (s,k)) . db = s . db ) by SCMFSA_3:11, SCMFSA_3:12;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A50, COMPOS_1:92
.= (s . f) +* (m,(s . da)) by A52, A54, A55, SCMFSA_3:11, A56
.= (IncIC ((Exec (INS,s)),k)) . g by A53, A55, SCMFSA_3:12
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A50, COMPOS_1:92 ; :: thesis: verum
end;
suppose A57: 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 A50, COMPOS_1:92
.= (IncIC (s,k)) . g by A50, A57, SCMFSA_2:99
.= s . g by SCMFSA_3:12
.= (Exec (INS,s)) . g by A50, A57, SCMFSA_2:99
.= (Exec ((IncAddr (INS,j)),s)) . g by A50, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:12 ; :: thesis: verum
end;
end;
end;
now
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 A50, COMPOS_1:92
.= (IncIC (s,k)) . d by A50, SCMFSA_2:99
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A50, SCMFSA_2:99
.= (Exec ((IncAddr (INS,j)),s)) . d by A50, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A51, SCMFSA_2:138, A1; :: thesis: verum
end;
suppose InsCode INS = 11 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da being Int-Location , f being FinSeq-Location such that
A58: INS = da :=len f by SCMFSA_2:64;
A59: now
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 A58, COMPOS_1:92
.= (IncIC (s,k)) . f by A58, SCMFSA_2:100
.= s . f by SCMFSA_3:12
.= (Exec (INS,s)) . f by A58, SCMFSA_2:100
.= (Exec ((IncAddr (INS,j)),s)) . f by A58, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . f by SCMFSA_3:12 ; :: thesis: verum
end;
now
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 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 A58, COMPOS_1:92
.= len ((IncIC (s,k)) . f) by A60, A58, SCMFSA_2:100
.= len (s . f) by SCMFSA_3:12
.= (Exec (INS,s)) . d by A58, A60, SCMFSA_2:100
.= (IncIC ((Exec (INS,s)),k)) . d by SCMFSA_3:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by A58, COMPOS_1:92 ; :: thesis: verum
end;
suppose A61: 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 A58, COMPOS_1:92
.= (IncIC (s,k)) . d by A58, A61, SCMFSA_2:100
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A58, A61, SCMFSA_2:100
.= (Exec ((IncAddr (INS,j)),s)) . d by A58, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
end;
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A59, SCMFSA_2:138, A1; :: thesis: verum
end;
suppose InsCode INS = 12 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da being Int-Location , f being FinSeq-Location such that
A62: INS = f :=<0,...,0> da by SCMFSA_2:65;
A63: now
let g be FinSeq-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A64: ( ex m being Element of NAT st
( m = abs (s . da) & (Exec (INS,s)) . f = m |-> 0 ) & ex m being Element of NAT st
( m = abs ((IncIC (s,k)) . da) & (Exec (INS,(IncIC (s,k)))) . f = m |-> 0 ) ) by A62, SCMFSA_2:101;
per cases ( f = g or f <> g ) ;
suppose A65: f = g ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A66: (IncIC (s,k)) . da = s . da by SCMFSA_3:11;
thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . g = (Exec (INS,(IncIC (s,k)))) . g by A62, COMPOS_1:92
.= (IncIC ((Exec (INS,s)),k)) . g by A64, A65, SCMFSA_3:12, A66
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A62, COMPOS_1:92 ; :: thesis: verum
end;
suppose A67: 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 A62, COMPOS_1:92
.= (IncIC (s,k)) . g by A62, A67, SCMFSA_2:101
.= s . g by SCMFSA_3:12
.= (Exec (INS,s)) . g by A62, A67, SCMFSA_2:101
.= (Exec ((IncAddr (INS,j)),s)) . g by A62, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:12 ; :: thesis: verum
end;
end;
end;
now
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 A62, COMPOS_1:92
.= (IncIC (s,k)) . d by A62, SCMFSA_2:101
.= s . d by SCMFSA_3:11
.= (Exec (INS,s)) . d by A62, SCMFSA_2:101
.= (Exec ((IncAddr (INS,j)),s)) . d by A62, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:11 ; :: thesis: verum
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A63, SCMFSA_2:138, A1; :: thesis: verum
end;
suppose InsCode INS = 13 ; :: thesis: NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k))
then consider da being Int-Location such that
A62: INS = da :==1 by SCMFSA_2:134;
A63: now
let g be Int-Location ; :: thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1
A64: ( (Exec (INS,s)) . da = 1 & (Exec (INS,(IncIC (s,k)))) . da = 1 ) by A62, SCMFSA_2:136;
per cases ( da = g or da <> g ) ;
suppose A65: da = 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 A62, COMPOS_1:92
.= (IncIC ((Exec (INS,s)),k)) . g by A64, A65, SCMFSA_3:11
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by A62, COMPOS_1:92 ; :: thesis: verum
end;
suppose A67: da <> 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 A62, COMPOS_1:92
.= (IncIC (s,k)) . g by A62, A67, SCMFSA_2:136
.= s . g by SCMFSA_3:11
.= (Exec (INS,s)) . g by A62, A67, SCMFSA_2:136
.= (Exec ((IncAddr (INS,j)),s)) . g by A62, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . g by SCMFSA_3:11 ; :: thesis: verum
end;
end;
end;
now
let d be FinSeq-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 A62, COMPOS_1:92
.= (IncIC (s,k)) . d by A62, SCMFSA_2:136
.= s . d by SCMFSA_3:12
.= (Exec (INS,s)) . d by A62, SCMFSA_2:136
.= (Exec ((IncAddr (INS,j)),s)) . d by A62, COMPOS_1:92
.= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by SCMFSA_3:12 ; :: thesis: verum
end;
hence NPP (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) by A63, SCMFSA_2:138, A1; :: thesis: verum
end;
end;