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 that
A1: ( qe is one-to-one & rng qe c= rng pe ) and
A2: W is_weight>=0of G ; :: thesis: cost qe,W <= cost pe,W
defpred S₁[ 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;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[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 that
A5: q is one-to-one and
A6: rng q c= rng p and
A7: len q = k + 1 ; :: thesis: cost q,W <= cost p,W
consider q1 being FinSequence, x being set such that
A8: q = q1 ^ <*x*> by A7, FINSEQ_2:21;
A9: k + 1 = (len q1) + 1 by A7, A8, FINSEQ_2:19;
consider p1, p2 being FinSequence such that
A10: p = (p1 ^ <*x*>) ^ p2 and
A11: rng q1 c= rng (p1 ^ p2) by A5, A6, A8, Th12;
reconsider q1 = q1 as FinSequence of the carrier' of G by A8, FINSEQ_1:50;
A12: p1 ^ <*x*> is FinSequence of the carrier' of G by A10, FINSEQ_1:50;
then reconsider y = <*x*> as FinSequence of the carrier' of G by FINSEQ_1:50;
reconsider p2 = p2 as FinSequence of the carrier' of G by A10, FINSEQ_1:50;
reconsider p1 = p1 as FinSequence of the carrier' of G by A12, FINSEQ_1:50;
q1 is one-to-one by A5, A8, FINSEQ_3:98;
then A13: cost q1,W <= cost (p1 ^ p2),W by A4, A11, A9;
A14: cost q,W = (cost q1,W) + (cost y,W) by A2, A8, Th50, Th58;
cost p,W = (cost (p1 ^ y),W) + (cost p2,W) by A2, A10, Th50, Th58
.= ((cost p1,W) + (cost y,W)) + (cost p2,W) by A2, Th50, Th58
.= ((cost p1,W) + (cost p2,W)) + (cost y,W)
.= (cost (p1 ^ p2),W) + (cost y,W) by A2, Th50, Th58 ;
hence cost q,W <= cost p,W by A14, A13, XREAL_1:9; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A15: S₁[ 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 that
q is one-to-one and
rng q c= rng p and
A16: len q = 0 ; :: thesis: cost q,W <= cost p,W
q = {} by A16;
then cost q,W = 0 by A2, Th50, Th55;
hence cost q,W <= cost p,W by A2, Th54; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A15, A3);
then S₁[ len qe] ;
hence cost qe,W <= cost pe,W by A1; :: thesis: verum