let k be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined FinPartState of S holds dom F, dom (Shift F,k) are_equipotent
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N
for F being NAT -defined FinPartState of S holds dom F, dom (Shift F,k) are_equipotent
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of NAT ,N; :: thesis: for F being NAT -defined FinPartState of S holds dom F, dom (Shift F,k) are_equipotent
let F be NAT -defined FinPartState of S; :: thesis: dom F, dom (Shift F,k) are_equipotent
A1:
dom F c= NAT
by RELAT_1:def 18;
defpred S1[ set , set ] means ex il being Instruction-Location of S st
( $1 = il & $2 = il. S,(k + (locnum il)) );
A2:
for e being set st e in dom F holds
ex u being set st S1[e,u]
proof
let e be
set ;
:: thesis: ( e in dom F implies ex u being set st S1[e,u] )
assume
e in dom F
;
:: thesis: ex u being set st S1[e,u]
then reconsider e =
e as
Instruction-Location of
S by A1, AMI_1:def 4;
take
il. S,
(k + (locnum e))
;
:: thesis: S1[e, il. S,(k + (locnum e))]
take
e
;
:: thesis: ( e = e & il. S,(k + (locnum e)) = il. S,(k + (locnum e)) )
thus
(
e = e &
il. S,
(k + (locnum e)) = il. S,
(k + (locnum e)) )
;
:: thesis: verum
end;
consider f being Function such that
A3:
dom f = dom F
and
A4:
for x being set st x in dom F holds
S1[x,f . x]
from CLASSES1:sch 1(A2);
take
f
; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = dom F & rng f = dom (Shift F,k) )
hereby :: according to FUNCT_1:def 8 :: thesis: ( dom f = dom F & rng f = dom (Shift F,k) )
let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )assume that A5:
x1 in dom f
and A6:
x2 in dom f
and A7:
f . x1 = f . x2
;
:: thesis: x1 = x2consider i1 being
Instruction-Location of
S such that A8:
x1 = i1
and A9:
f . x1 = il. S,
(k + (locnum i1))
by A3, A4, A5;
consider i2 being
Instruction-Location of
S such that A10:
x2 = i2
and A11:
f . x2 = il. S,
(k + (locnum i2))
by A3, A4, A6;
k + (locnum i1) = k + (locnum i2)
by A7, A9, A11, AMISTD_1:25;
hence
x1 = x2
by A8, A10, AMISTD_1:27;
:: thesis: verum
end;
thus
dom f = dom F
by A3; :: thesis: rng f = dom (Shift F,k)
A12:
dom (Shift F,k) = { (il. S,(m + k)) where m is Element of NAT : il. S,m in dom F }
by Def16;
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: dom (Shift F,k) c= rng f
let y be
set ;
:: thesis: ( y in rng f implies y in dom (Shift F,k) )assume
y in rng f
;
:: thesis: y in dom (Shift F,k)then consider x being
set such that A13:
x in dom f
and A14:
f . x = y
by FUNCT_1:def 5;
consider il being
Instruction-Location of
S such that A15:
(
x = il &
f . x = il. S,
(k + (locnum il)) )
by A3, A4, A13;
consider a being
natural number such that A16:
il = il. S,
a
by AMISTD_1:26;
reconsider a =
a as
Element of
NAT by ORDINAL1:def 13;
a = locnum il
by A16, AMISTD_1:def 13;
hence
y in dom (Shift F,k)
by A3, A12, A13, A14, A15, A16;
:: thesis: verum
end;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (Shift F,k) or y in rng f )
assume
y in dom (Shift F,k)
; :: thesis: y in rng f
then consider m being Element of NAT such that
A17:
y = il. S,(m + k)
and
A18:
il. S,m in dom F
by A12;
consider il being Instruction-Location of S such that
A19:
( il. S,m = il & f . (il. S,m) = il. S,(k + (locnum il)) )
by A4, A18;
m = locnum il
by A19, AMISTD_1:def 13;
hence
y in rng f
by A3, A17, A18, A19, FUNCT_1:def 5; :: thesis: verum