defpred S1[ Nat] means for W1 being DWalk of G st W1 .length() = G holds
ex W2 being Path of W1 st W2 is directed ;
A1:
W .length() = W .length()
;
now for k being Nat st S1[k] holds
for W1 being DWalk of G st W1 .length() = k + 1 holds
ex W2 being Path of W1 st W2 is directed let k be
Nat;
( S1[k] implies for W1 being DWalk of G st W1 .length() = k + 1 holds
ex W2 being Path of W1 st W2 is directed )assume A2:
S1[
k]
;
for W1 being DWalk of G st W1 .length() = k + 1 holds
ex W2 being Path of W1 st W2 is directed let W1 be
DWalk of
G;
( W1 .length() = k + 1 implies ex W2 being Path of W1 st W2 is directed )set WA =
W1 .cut (1,
((2 * k) + 1));
set e =
W1 . (((2 * k) + 1) + 1);
set v =
W1 . (((2 * k) + 1) + 2);
assume A3:
W1 .length() = k + 1
;
ex W2 being Path of W1 st W2 is directed then A4:
len W1 =
(2 * (k + 1)) + 1
by Def15
.=
((2 * k) + 1) + 2
;
then A5:
(((2 * k) + 1) + 2) - 2
< (len W1) - 0
by XREAL_1:15;
then A6:
W1 . (((2 * k) + 1) + 1) DJoins W1 . ((2 * k) + 1),
W1 . (((2 * k) + 1) + 2),
G
by Lm51;
len (W1 .cut (1,((2 * k) + 1))) = (2 * k) + 1
by A5, Lm22;
then A7:
(2 * k) + 1
= (2 * ((W1 .cut (1,((2 * k) + 1))) .length())) + 1
by Def15;
then consider WB being
Path of
W1 .cut (1,
((2 * k) + 1))
such that A8:
WB is
directed
by A2;
A9:
(W1 .cut (1,((2 * k) + 1))) .edgeSeq() c= W1 .edgeSeq()
by Lm43;
A10:
WB is_Walk_from (W1 .cut (1,((2 * k) + 1))) .first() ,
(W1 .cut (1,((2 * k) + 1))) .last()
by Def32;
A11:
1
<= (2 * k) + 1
by NAT_1:12;
then A12:
(W1 .cut (1,((2 * k) + 1))) .last() = W1 . ((2 * k) + 1)
by A5, Lm16, JORDAN12:2;
A13:
(W1 .cut (1,((2 * k) + 1))) .first() = W1 . 1
by A5, A11, Lm16, JORDAN12:2;
then A14:
WB .first() = W1 . 1
by A10;
A15:
WB .last() = W1 . ((2 * k) + 1)
by A10, A12;
then A16:
W1 . (((2 * k) + 1) + 1) Joins WB .last() ,
W1 . (((2 * k) + 1) + 2),
G
by A6, GLIB_000:16;
now ex W2 being Path of W1 st W2 is directed per cases
( WB is closed or WB is open )
;
suppose A17:
WB is
closed
;
ex W2 being Path of W1 st W2 is directed set W2 =
W1 .remove (1,
((2 * k) + 1));
W1 .first() = W1 . ((2 * k) + 1)
by A14, A15, A17;
then
W1 .remove (1,
((2 * k) + 1))
= W1 .cut (
((2 * k) + 1),
(((2 * k) + 1) + 2))
by A4, Lm32;
then (len (W1 .remove (1,((2 * k) + 1)))) + ((2 * k) + 1) =
(((2 * k) + 1) + 2) + 1
by A4, A5, Lm15
.=
((2 * k) + 1) + (2 + 1)
;
then reconsider W2 =
W1 .remove (1,
((2 * k) + 1)) as
Path of
W1 by Lm69;
take W2 =
W2;
W2 is directed thus
W2 is
directed
;
verum end; suppose A18:
WB is
open
;
ex W2 being Path of W1 st W2 is directed consider esb being
Subset of
((W1 .cut (1,((2 * k) + 1))) .edgeSeq()) such that A19:
WB .edgeSeq() = Seq esb
by Def32;
A20:
Seq esb is
one-to-one
by A19, Def27;
A21:
Seq esb = esb * (Sgm (dom esb))
by FINSEQ_1:def 14;
then A23:
dom esb c= Seg k
by TARSKI:def 3;
then
rng (Sgm (dom esb)) = dom esb
by FINSEQ_1:def 13;
then A24:
Sgm (dom esb) is
one-to-one
by A21, A20, FUNCT_1:26;
now ex W2 being Path of W1 st W2 is directed per cases
( W1 . (((2 * k) + 1) + 2) in WB .vertices() or not W1 . (((2 * k) + 1) + 2) in WB .vertices() )
;
suppose A25:
W1 . (((2 * k) + 1) + 2) in WB .vertices()
;
ex W2 being Path of W1 st W2 is directed reconsider WB9 =
WB as
directed Path of
G by A8;
A26:
dom (Sgm (dom esb)) =
dom (WB .edgeSeq())
by A19, Th5
.=
Seg (len (WB .edgeSeq()))
by FINSEQ_1:def 3
;
consider n being
odd Element of
NAT such that A27:
n <= len WB
and A28:
WB . n = W1 . (((2 * k) + 1) + 2)
by A25, Lm45;
set W2 =
WB9 .cut (1,
n);
len (WB9 .cut (1,n)) = n
by A27, Lm22;
then consider naa1 being
even Element of
NAT such that A29:
naa1 = n - 1
and A30:
len ((WB9 .cut (1,n)) .edgeSeq()) = naa1 div 2
by Lm42;
(2 * 0) + 1
<= n
by ABIAN:12;
then A31:
WB9 .cut (1,
n)
is_Walk_from W1 .first() ,
W1 .last()
by A4, A14, A27, A28, Lm16;
2
divides naa1
by PEPIN:22;
then A32:
2
* (naa1 div 2) = naa1
by NAT_D:3;
then
Seg (naa1 div 2) c= dom (Sgm (dom esb))
by A26, FINSEQ_1:5;
then A33:
dom ((Sgm (dom esb)) | (Seg (naa1 div 2))) = Seg (naa1 div 2)
by RELAT_1:62;
reconsider ses =
(Sgm (dom esb)) | (Seg (naa1 div 2)) as
FinSequence ;
A34:
ses is
one-to-one
by A24, FUNCT_1:52;
set es =
esb | (rng ((Sgm (dom esb)) | (Seg (naa1 div 2))));
reconsider es =
esb | (rng ((Sgm (dom esb)) | (Seg (naa1 div 2)))) as
Subset of
((W1 .cut (1,((2 * k) + 1))) .edgeSeq()) by FINSEQ_6:153;
for
x being
object st
x in es holds
x in W1 .edgeSeq()
by A9, TARSKI:def 3;
then reconsider es =
es as
Subset of
(W1 .edgeSeq()) by TARSKI:def 3;
reconsider esbes1 =
esb \ es as
Function ;
then
rng ((Sgm (dom esb)) | (Seg (naa1 div 2))) c= dom esb
by TARSKI:def 3;
then A36:
dom es = rng ((Sgm (dom esb)) | (Seg (naa1 div 2)))
by RELAT_1:62;
A37:
now for a, b being Nat st a in dom es & b in dom esbes1 holds
a < blet a,
b be
Nat;
( a in dom es & b in dom esbes1 implies a < b )assume that A38:
a in dom es
and A39:
b in dom esbes1
;
a < bconsider xa being
object such that A40:
xa in dom ses
and A41:
ses . xa = a
by A36, A38, FUNCT_1:def 3;
reconsider xa =
xa as
Element of
NAT by A40;
A42:
xa in Seg (naa1 div 2)
by A40, RELAT_1:57;
then A43:
1
<= xa
by FINSEQ_1:1;
A44:
[b,(esbes1 . b)] in esb \ es
by A39, FUNCT_1:1;
then A45:
[b,(esbes1 . b)] in esb
by XBOOLE_0:def 5;
then
b in dom esb
by FUNCT_1:1;
then
b in rng (Sgm (dom esb))
by A23, FINSEQ_1:def 13;
then consider xb being
object such that A46:
xb in dom (Sgm (dom esb))
and A47:
(Sgm (dom esb)) . xb = b
by FUNCT_1:def 3;
reconsider xb =
xb as
Element of
NAT by A46;
A48:
1
<= xb
by A26, A46, FINSEQ_1:1;
A49:
xa <= naa1 div 2
by A42, FINSEQ_1:1;
A50:
now not xb <= xaassume
xb <= xa
;
contradictionthen
xb <= naa1 div 2
by A49, XXREAL_0:2;
then A51:
xb in Seg (naa1 div 2)
by A48, FINSEQ_1:1;
[xb,b] in Sgm (dom esb)
by A46, A47, FUNCT_1:1;
then
[xb,b] in ses
by A51, RELAT_1:def 11;
then
b in rng ses
by XTUPLE_0:def 13;
then
[b,(esbes1 . b)] in es
by A45, RELAT_1:def 11;
hence
contradiction
by A44, XBOOLE_0:def 5;
verum end;
xb <= len (WB .edgeSeq())
by A26, A46, FINSEQ_1:1;
then
xb in dom (Seq esb)
by A19, A48, FINSEQ_3:25;
then
xb in dom (Sgm (dom esb))
by Th5;
then A52:
xb <= len (Sgm (dom esb))
by FINSEQ_3:25;
a = (Sgm (dom esb)) . xa
by A40, A41, FUNCT_1:47;
hence
a < b
by A23, A47, A43, A52, A50, FINSEQ_1:def 13;
verum end;
len ses = naa1 div 2
by A33, FINSEQ_1:def 3;
then
card (dom es) = naa1 div 2
by A36, A34, FINSEQ_4:62;
then
card es = naa1 div 2
by CARD_1:62;
then A53:
len (Seq es) = len ((WB9 .cut (1,n)) .edgeSeq())
by A30, Th4;
A54:
es c= esb
by RELAT_1:59;
now for z being object holds
( ( z in esb implies z in es \/ (esb \ es) ) & ( z in es \/ (esb \ es) implies z in esb ) )let z be
object ;
( ( z in esb implies z in es \/ (esb \ es) ) & ( z in es \/ (esb \ es) implies z in esb ) )hereby ( z in es \/ (esb \ es) implies z in esb )
assume A55:
z in esb
;
z in es \/ (esb \ es)hence
z in es \/ (esb \ es)
;
verum
end; assume A56:
z in es \/ (esb \ es)
;
z in esbhence
z in esb
;
verum end; then
esb = es \/ (esb \ es)
by TARSKI:2;
then A57:
dom esb = (dom es) \/ (dom (esb \ es))
by XTUPLE_0:23;
esb \ es c= esb
by XBOOLE_1:36;
then
dom (esb \ es) c= dom esb
by RELAT_1:11;
then A58:
dom (esb \ es) c= Seg k
by A23, XBOOLE_1:1;
dom es c= dom esb
by A54, RELAT_1:11;
then
dom es c= Seg k
by A23, XBOOLE_1:1;
then A59:
Sgm (dom esb) = (Sgm (dom es)) ^ (Sgm (dom (esb \ es)))
by A57, A58, A37, FINSEQ_3:42;
A60:
(WB9 .cut (1,n)) .edgeSeq() c= WB .edgeSeq()
by Lm43;
then A61:
dom ((WB9 .cut (1,n)) .edgeSeq()) c= dom (Seq esb)
by A19, RELAT_1:11;
A62:
Seq es = es * (Sgm (dom es))
by FINSEQ_1:def 14;
now for x being Nat st 1 <= x & x <= len ((WB9 .cut (1,n)) .edgeSeq()) holds
((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . xlet x be
Nat;
( 1 <= x & x <= len ((WB9 .cut (1,n)) .edgeSeq()) implies ((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . x )assume that A63:
1
<= x
and A64:
x <= len ((WB9 .cut (1,n)) .edgeSeq())
;
((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . xA65:
x in dom ((WB9 .cut (1,n)) .edgeSeq())
by A63, A64, FINSEQ_3:25;
then
x in dom (Sgm (dom esb))
by A21, A61, FUNCT_1:11;
then A66:
[x,((Sgm (dom esb)) . x)] in Sgm (dom esb)
by FUNCT_1:1;
x in Seg (naa1 div 2)
by A30, A63, A64, FINSEQ_1:1;
then
[x,((Sgm (dom esb)) . x)] in ses
by A66, RELAT_1:def 11;
then A67:
(Sgm (dom esb)) . x in rng ses
by XTUPLE_0:def 13;
(Sgm (dom esb)) . x in dom esb
by A21, A61, A65, FUNCT_1:11;
then
[((Sgm (dom esb)) . x),(esb . ((Sgm (dom esb)) . x))] in esb
by FUNCT_1:1;
then A68:
[((Sgm (dom esb)) . x),(esb . ((Sgm (dom esb)) . x))] in es
by A67, RELAT_1:def 11;
[x,(((WB9 .cut (1,n)) .edgeSeq()) . x)] in (WB9 .cut (1,n)) .edgeSeq()
by A65, FUNCT_1:1;
then A69:
((WB9 .cut (1,n)) .edgeSeq()) . x =
(Seq esb) . x
by A19, A60, FUNCT_1:1
.=
esb . ((Sgm (dom esb)) . x)
by A21, A61, A65, FUNCT_1:12
;
A70:
x in dom (Seq es)
by A53, A63, A64, FINSEQ_3:25;
then
x in dom (Sgm (dom es))
by Th5;
then
(Sgm (dom esb)) . x = (Sgm (dom es)) . x
by A59, FINSEQ_1:def 7;
then
es . ((Sgm (dom es)) . x) = esb . ((Sgm (dom esb)) . x)
by A68, FUNCT_1:1;
hence
((WB9 .cut (1,n)) .edgeSeq()) . x = (Seq es) . x
by A62, A69, A70, FUNCT_1:12;
verum end; then
(WB9 .cut (1,n)) .edgeSeq() = Seq es
by A53, FINSEQ_1:14;
then reconsider W2 =
WB9 .cut (1,
n) as
Path of
W1 by A31, Def32;
take W2 =
W2;
W2 is directed thus
W2 is
directed
;
verum end; suppose A71:
not
W1 . (((2 * k) + 1) + 2) in WB .vertices()
;
ex W2 being Path of W1 st W2 is directed set es =
esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)));
set W2 =
WB .addEdge (W1 . (((2 * k) + 1) + 1));
A76:
dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) = {(k + 1)}
;
then A77:
dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) = (dom esb) \/ {(k + 1)}
by FUNCT_4:def 1;
then A83:
dom (esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))) c= Seg (k + 1)
by TARSKI:def 3;
then reconsider es =
esb +* ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) as
FinSubsequence by FINSEQ_1:def 12;
now for z being object st z in es holds
z in W1 .edgeSeq() let z be
object ;
( z in es implies z in W1 .edgeSeq() )assume A84:
z in es
;
z in W1 .edgeSeq() then consider x,
y being
object such that A85:
z = [x,y]
by RELAT_1:def 1;
A86:
x in dom es
by A84, A85, FUNCT_1:1;
A87:
es . x = y
by A84, A85, FUNCT_1:1;
now z in W1 .edgeSeq() per cases
( x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) or not x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) )
;
suppose A88:
x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))
;
z in W1 .edgeSeq() then reconsider x9 =
x as
Element of
NAT by A76;
A89:
x = k + 1
by A88, TARSKI:def 1;
then A90:
1
<= x9
by NAT_1:12;
then A91:
x in dom (W1 .edgeSeq())
by A3, A89, FINSEQ_3:25;
y = ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) . x
by A77, A86, A87, A88, FUNCT_4:def 1;
then A92:
y = W1 . (((2 * k) + 1) + 1)
by A89, FUNCOP_1:72;
(W1 .edgeSeq()) . x =
W1 . (2 * (k + 1))
by A3, A89, A90, Def15
.=
W1 . (((2 * k) + 1) + 1)
;
hence
z in W1 .edgeSeq()
by A85, A92, A91, FUNCT_1:1;
verum end; suppose A93:
not
x in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))
;
z in W1 .edgeSeq() then A94:
x in dom esb
by A77, A86, XBOOLE_0:def 3;
y = esb . x
by A77, A86, A87, A93, FUNCT_4:def 1;
then
[x,y] in esb
by A94, FUNCT_1:1;
then
[x,y] in (W1 .cut (1,((2 * k) + 1))) .edgeSeq()
;
hence
z in W1 .edgeSeq()
by A9, A85;
verum end; end; end; hence
z in W1 .edgeSeq()
;
verum end; then reconsider es =
es as
Subset of
(W1 .edgeSeq()) by TARSKI:def 3;
{(k + 1)} c= Seg (k + 1)
by A77, A83, XBOOLE_1:11;
then A95:
Sgm (dom es) =
(Sgm (dom esb)) ^ (Sgm {(k + 1)})
by A23, A77, A72, FINSEQ_3:42
.=
(Sgm (dom esb)) ^ <*(k + 1)*>
by FINSEQ_3:44
;
then A98:
dom esb misses dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))
by XBOOLE_0:def 7;
A99:
(WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq() = (Seq esb) ^ <*(W1 . (((2 * k) + 1) + 1))*>
by A16, A19, Lm44;
then A100:
len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) =
(len (Seq esb)) + (len <*(W1 . (((2 * k) + 1) + 1))*>)
by FINSEQ_1:22
.=
(len (Seq esb)) + 1
by FINSEQ_1:39
.=
(card esb) + 1
by Th4
;
A101:
len (Seq es) =
card es
by Th4
.=
(card esb) + (card ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))))
by A98, PRE_CIRC:22
.=
(card esb) + (card {[(k + 1),(W1 . (((2 * k) + 1) + 1))]})
by FUNCT_4:82
.=
len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq())
by A100, CARD_1:30
;
now for n being Nat st 1 <= n & n <= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) holds
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . nA102:
Seq es = es * (Sgm (dom es))
by FINSEQ_1:def 14;
let n be
Nat;
( 1 <= n & n <= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) implies ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n )assume that A103:
1
<= n
and A104:
n <= len ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq())
;
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
n in dom (Seq es)
by A101, A103, A104, FINSEQ_3:25;
then A105:
(Seq es) . n = es . ((Sgm (dom es)) . n)
by A102, FUNCT_1:12;
A106:
Seq esb = esb * (Sgm (dom esb))
by FINSEQ_1:def 14;
A107:
n in dom ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq())
by A103, A104, FINSEQ_3:25;
now ((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . nper cases
( n in dom (Seq esb) or ex m being Nat st
( m in dom <*(W1 . (((2 * k) + 1) + 1))*> & n = (len (Seq esb)) + m ) )
by A99, A107, FINSEQ_1:25;
suppose A108:
n in dom (Seq esb)
;
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . nthen
n in dom (Sgm (dom esb))
by A106, FUNCT_1:11;
then A109:
(Sgm (dom es)) . n = (Sgm (dom esb)) . n
by A95, FINSEQ_1:def 7;
A110:
(Sgm (dom esb)) . n in dom esb
by A106, A108, FUNCT_1:11;
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n =
(Seq esb) . n
by A99, A108, FINSEQ_1:def 7
.=
esb . ((Sgm (dom esb)) . n)
by A106, A108, FUNCT_1:12
;
hence
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
by A98, A105, A110, A109, FUNCT_4:16;
verum end; suppose
ex
m being
Nat st
(
m in dom <*(W1 . (((2 * k) + 1) + 1))*> &
n = (len (Seq esb)) + m )
;
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . nthen consider m being
Nat such that A111:
m in dom <*(W1 . (((2 * k) + 1) + 1))*>
and A112:
n = (len (Seq esb)) + m
;
m in {1}
by A111, FINSEQ_1:2, FINSEQ_1:def 8;
then A113:
m = 1
by TARSKI:def 1;
A114:
k + 1
in dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1)))
by TARSKI:def 1;
then A115:
k + 1
in (dom esb) \/ (dom ((k + 1) .--> (W1 . (((2 * k) + 1) + 1))))
by XBOOLE_0:def 3;
len (Sgm (dom esb)) =
card (dom esb)
by A23, FINSEQ_3:39
.=
card esb
by CARD_1:62
.=
len (Seq esb)
by Th4
;
then
(Seq es) . n = es . (k + 1)
by A95, A105, A112, A113, FINSEQ_1:42;
then A116:
(Seq es) . n =
((k + 1) .--> (W1 . (((2 * k) + 1) + 1))) . (k + 1)
by A114, A115, FUNCT_4:def 1
.=
W1 . (((2 * k) + 1) + 1)
by FUNCOP_1:72
;
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n =
<*(W1 . (((2 * k) + 1) + 1))*> . 1
by A99, A111, A112, A113, FINSEQ_1:def 7
.=
W1 . (((2 * k) + 1) + 1)
by FINSEQ_1:def 8
;
hence
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
by A116;
verum end; end; end; hence
((WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq()) . n = (Seq es) . n
;
verum end; then A117:
(WB .addEdge (W1 . (((2 * k) + 1) + 1))) .edgeSeq() = Seq es
by A101, FINSEQ_1:14;
WB .addEdge (W1 . (((2 * k) + 1) + 1)) is_Walk_from W1 .first() ,
W1 .last()
by A4, A8, A6, A10, A13, A12, Lm52;
then reconsider W2 =
WB .addEdge (W1 . (((2 * k) + 1) + 1)) as
Path of
W1 by A16, A18, A71, A117, Def32, Lm68;
take W2 =
W2;
W2 is directed thus
W2 is
directed
by A8, A6, A10, A12, Lm52;
verum end; end; end; hence
ex
W2 being
Path of
W1 st
W2 is
directed
;
verum end; end; end; hence
ex
W2 being
Path of
W1 st
W2 is
directed
;
verum end;
then A118:
for k being Nat st S1[k] holds
S1[k + 1]
;
then A120:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A120, A118);
hence
ex b1 being Path of W st b1 is directed
by A1; verum