let W be Function; :: thesis: for G being Graph
for qe, pe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds
cost qe,W <= cost pe,W
let G be Graph; :: thesis: for qe, pe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds
cost qe,W <= cost pe,W
let qe, pe be FinSequence of the carrier' of G; :: thesis: ( qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G implies cost qe,W <= cost pe,W )
set D = the carrier' of G;
assume A1:
( qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G )
; :: thesis: cost qe,W <= cost pe,W
defpred S1[ Nat] means for p, q being FinSequence of the carrier' of G st q is one-to-one & rng q c= rng p & len q = $1 holds
cost q,W <= cost p,W;
A2:
S1[ 0 ]
proof
let p,
q be
FinSequence of the
carrier' of
G;
:: thesis: ( q is one-to-one & rng q c= rng p & len q = 0 implies cost q,W <= cost p,W )
assume
(
q is
one-to-one &
rng q c= rng p &
len q = 0 )
;
:: thesis: cost q,W <= cost p,W
then
q = {}
;
then
cost q,
W = 0
by A1, Th50, Th55;
hence
cost q,
W <= cost p,
W
by A1, Th54;
:: thesis: verum
end;
A3:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
:: thesis: S1[k + 1]
now let p,
q be
FinSequence of the
carrier' of
G;
:: thesis: ( q is one-to-one & rng q c= rng p & len q = k + 1 implies cost q,W <= cost p,W )assume A5:
(
q is
one-to-one &
rng q c= rng p &
len q = k + 1 )
;
:: thesis: cost q,W <= cost p,Wthen consider q1 being
FinSequence,
x being
set such that A6:
q = q1 ^ <*x*>
by FINSEQ_2:21;
consider p1,
p2 being
FinSequence such that A7:
(
p = (p1 ^ <*x*>) ^ p2 &
rng q1 c= rng (p1 ^ p2) )
by A5, A6, Th12;
A8:
k + 1
= (len q1) + 1
by A5, A6, FINSEQ_2:19;
A9:
p1 ^ <*x*> is
FinSequence of the
carrier' of
G
by A7, FINSEQ_1:50;
then reconsider p1 =
p1 as
FinSequence of the
carrier' of
G by FINSEQ_1:50;
reconsider y =
<*x*> as
FinSequence of the
carrier' of
G by A9, FINSEQ_1:50;
reconsider p2 =
p2 as
FinSequence of the
carrier' of
G by A7, FINSEQ_1:50;
reconsider q1 =
q1 as
FinSequence of the
carrier' of
G by A6, FINSEQ_1:50;
A10:
cost q,
W = (cost q1,W) + (cost y,W)
by A1, A6, Th50, Th58;
A11:
cost p,
W =
(cost (p1 ^ y),W) + (cost p2,W)
by A1, A7, Th50, Th58
.=
((cost p1,W) + (cost y,W)) + (cost p2,W)
by A1, Th50, Th58
.=
((cost p1,W) + (cost p2,W)) + (cost y,W)
.=
(cost (p1 ^ p2),W) + (cost y,W)
by A1, Th50, Th58
;
q1 is
one-to-one
by A5, A6, FINSEQ_3:98;
then
cost q1,
W <= cost (p1 ^ p2),
W
by A4, A7, A8;
hence
cost q,
W <= cost p,
W
by A10, A11, XREAL_1:9;
:: thesis: verum end;
hence
S1[
k + 1]
;
:: thesis: verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A2, A3);
then
S1[ len qe]
;
hence
cost qe,W <= cost pe,W
by A1; :: thesis: verum