let m be Element of NAT ; :: thesis: for I being preProgram of SCM+FSA holds card (ProgramPart (Relocated I,m)) = card I
let I be preProgram of SCM+FSA ; :: thesis: card (ProgramPart (Relocated I,m)) = card I
deffunc H1( Element of NAT ) -> Element of NAT = $1;
set B = { l where l is Element of NAT : H1(l) in dom I } ;
A1: for x being set st x in dom I holds
ex d being Element of NAT st x = H1(d)
proof
let x be set ; :: thesis: ( x in dom I implies ex d being Element of NAT st x = H1(d) )
A2: dom I c= NAT by RELAT_1:def 18;
assume x in dom I ; :: thesis: ex d being Element of NAT st x = H1(d)
then reconsider l = x as Instruction-Location of SCM+FSA by A2, AMI_1:def 4;
reconsider d = l as Element of NAT by ORDINAL1:def 13;
l = H1(d) ;
hence ex d being Element of NAT st x = H1(d) ; :: thesis: verum
end;
A3: for d1, d2 being Element of NAT st H1(d1) = H1(d2) holds
d1 = d2 ;
A4: dom I,{ l where l is Element of NAT : H1(l) in dom I } are_equipotent from FUNCT_7:sch 3(A1, A3);
 defpred S1[ Element of NAT ] means H1($1) in dom I;
set D = { l where l is Element of NAT : S1[l] } ;
{ l where l is Element of NAT : S1[l] } is Subset of NAT from DOMAIN_1:sch 7();
 then A5: { l where l is Element of NAT : H1(l) in dom I } c= NAT ;
deffunc H2( Element of NAT ) -> Element of NAT = $1 + m;
set C = { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } ;
A6: for d1, d2 being Element of NAT st H2(d1) = H2(d2) holds
d1 = d2 ;
A7: { l where l is Element of NAT : H1(l) in dom I } ,{ H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } are_equipotent from FUNCT_7:sch 4(A5, A6);
 defpred S2[ set ] means verum;
defpred S3[ Element of NAT ] means $1 in dom I;
set C = { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) } ;
set A = { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } ;
A8: { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) } = { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } from FRAENKEL:sch 14();
 A9: { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) } = { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } }
proof
thus { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) } c= { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } :: according to XBOOLE_0:def 10 :: thesis: { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } c= { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) }
proof
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) } or e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } )
assume e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) } ; :: thesis: e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } }
then ex l being Element of NAT st
( e = H2(l) & l in { l where l is Element of NAT : H1(l) in dom I } ) ;
hence e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } ; :: thesis: verum
end;
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } or e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) } )
assume e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } ; :: thesis: e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) }
then ex l being Element of NAT st
( e = l + m & l in { l where l is Element of NAT : H1(l) in dom I } ) ;
hence e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S3[n] } & S2[l] ) } ; :: thesis: verum
end;
{ H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } = { (l + m) where l is Element of NAT : l in dom I }
proof
thus { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } c= { (l + m) where l is Element of NAT : l in dom I } :: according to XBOOLE_0:def 10 :: thesis: { (l + m) where l is Element of NAT : l in dom I } c= { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) }
proof
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } or e in { (l + m) where l is Element of NAT : l in dom I } )
assume e in { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } ; :: thesis: e in { (l + m) where l is Element of NAT : l in dom I }
then ex l being Element of NAT st
( e = H2(l) & l in dom I ) ;
hence e in { (l + m) where l is Element of NAT : l in dom I } ; :: thesis: verum
end;
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (l + m) where l is Element of NAT : l in dom I } or e in { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } )
assume e in { (l + m) where l is Element of NAT : l in dom I } ; :: thesis: e in { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) }
then ex l being Element of NAT st
( e = l + m & l in dom I ) ;
hence e in { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } ; :: thesis: verum
end;
then dom (Shift I,m) = { H2(l) where l is Element of NAT : ( S3[l] & S2[l] ) } by VALUED_1:def 12;
then A10: dom (Shift I,m), dom I are_equipotent by A4, A7, A8, A9, WELLORD2:22;
thus card (ProgramPart (Relocated I,m)) = card (IncAddr [(Shift (ProgramPart I),m)],m) by SCMFSA_5:2
.= card (IncAddr (Shift I,m),m) by AMI_1:105
.= card (dom (IncAddr (Shift I,m),m)) by CARD_1:104
.= card (dom (Shift I,m)) by SCMFSA_4:def 6
.= card (dom I) by A10, CARD_1:21
.= card I by CARD_1:104 ; :: thesis: verum