let W be Function; for G being Graph
for pe, qe 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; for pe, qe 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 pe, qe be FinSequence of the carrier' of G; ( 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
; 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);
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
now for p, q being FinSequence of the carrier' of G st q is one-to-one & rng q c= rng p & len q = k + 1 holds
cost (q,W) <= cost (p,W)let p,
q be
FinSequence of the
carrier' of
G;
( 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
;
cost (q,W) <= cost (p,W)consider q1 being
FinSequence,
x being
object such that A8:
q = q1 ^ <*x*>
by A7, FINSEQ_2:18;
A9:
k + 1
= (len q1) + 1
by A7, A8, FINSEQ_2:16;
consider p1,
p2 being
FinSequence such that A10:
p = (p1 ^ <*x*>) ^ p2
and A11:
rng q1 c= rng (p1 ^ p2)
by A5, A6, A8, Th7;
reconsider q1 =
q1 as
FinSequence of the
carrier' of
G by A8, FINSEQ_1:36;
A12:
p1 ^ <*x*> is
FinSequence of the
carrier' of
G
by A10, FINSEQ_1:36;
then reconsider y =
<*x*> as
FinSequence of the
carrier' of
G by FINSEQ_1:36;
reconsider p2 =
p2 as
FinSequence of the
carrier' of
G by A10, FINSEQ_1:36;
reconsider p1 =
p1 as
FinSequence of the
carrier' of
G by A12, FINSEQ_1:36;
q1 is
one-to-one
by A5, A8, FINSEQ_3:91;
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, Th44, Th52;
cost (
p,
W) =
(cost ((p1 ^ y),W)) + (cost (p2,W))
by A2, A10, Th44, Th52
.=
((cost (p1,W)) + (cost (y,W))) + (cost (p2,W))
by A2, Th44, Th52
.=
((cost (p1,W)) + (cost (p2,W))) + (cost (y,W))
.=
(cost ((p1 ^ p2),W)) + (cost (y,W))
by A2, Th44, Th52
;
hence
cost (
q,
W)
<= cost (
p,
W)
by A14, A13, XREAL_1:7;
verum end;
hence
S1[
k + 1]
;
verum
end;
A15:
S1[ 0 ]
proof
let p,
q be
FinSequence of the
carrier' of
G;
( 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
;
cost (q,W) <= cost (p,W)
q = {}
by A16;
then
cost (
q,
W)
= 0
by A2, Th44, Th49;
hence
cost (
q,
W)
<= cost (
p,
W)
by A2, Th48;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A15, A3);
then
S1[ len qe]
;
hence
cost (qe,W) <= cost (pe,W)
by A1; verum