defpred S1[ Nat] means for W being DWalk of F1() st W .length() = $1 holds
P1[W];
A3:
S1[ 0 ]
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
let W be
DWalk of
F1();
( W .length() = k + 1 implies P1[W] )
assume A6:
W .length() = k + 1
;
P1[W]
then consider L being
odd Element of
NAT such that A7:
(
L = (len W) - 2 &
(W .cut (1,L)) .addEdge (W . (L + 1)) = W )
by GLIB_001:def 26, GLIB_001:133;
set W0 =
W .cut (1,
L);
A8:
L + 0 <= ((len W) - 2) + 2
by A7, XREAL_1:6;
then L =
len (W .cut (1,L))
by GLIB_001:45
.=
(2 * ((W .cut (1,L)) .length())) + 1
by GLIB_001:112
;
then (W .cut (1,L)) .length() =
(((len W) - 2) - 1) / 2
by A7
.=
((((2 * (W .length())) + 1) - 2) - 1) / 2
by GLIB_001:112
.=
(k + 1) - 1
by A6
;
then A9:
P1[
W .cut (1,
L)]
by A5;
(
W . (L + 1) in the_Edges_of F1() &
(the_Source_of F1()) . (W . (L + 1)) = (W .cut (1,L)) .last() )
proof
A10:
L + 0 < ((len W) - 2) + 2
by A7, XREAL_1:8;
then
W . (L + 1) Joins W . L,
W . (L + 2),
F1()
by GLIB_001:def 3;
hence
W . (L + 1) in the_Edges_of F1()
by GLIB_000:def 13;
(the_Source_of F1()) . (W . (L + 1)) = (W .cut (1,L)) .last()
A11:
L = len (W .cut (1,L))
by A8, GLIB_001:45;
then A12:
(W .cut (1,L)) . L = (W .cut (1,L)) .last()
by GLIB_001:def 7;
1
<= L
by ABIAN:12;
then
L in dom (W .cut (1,L))
by A11, FINSEQ_3:25;
then
W . L = (W .cut (1,L)) .last()
by A8, A12, GLIB_001:46;
hence
(the_Source_of F1()) . (W . (L + 1)) = (W .cut (1,L)) .last()
by A10, GLIB_001:def 25;
verum
end;
then
W . (L + 1) in ((W .cut (1,L)) .last()) .edgesOut()
by GLIB_000:58;
hence
P1[
W]
by A2, A7, A9;
verum
end;
A13:
for k being Nat holds S1[k]
from NAT_1:sch 2(A3, A4);
let W be DWalk of F1(); P1[W]
S1[W .length() ]
by A13;
hence
P1[W]
; verum