defpred S_{1}[ Nat] means for W being DWalk of F_{1}() st W .length() = $1 holds

P_{1}[W];

A3: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A3, A4);

let W be DWalk of F_{1}(); :: thesis: P_{1}[W]

S_{1}[W .length() ]
by A13;

hence P_{1}[W]
; :: thesis: verum

P

A3: S

proof

A4:
for k being Nat st S
let W be DWalk of F_{1}(); :: thesis: ( W .length() = 0 implies P_{1}[W] )

assume W .length() = 0 ; :: thesis: P_{1}[W]

then W is V5() by GLIB_001:def 26;

hence P_{1}[W]
by A1; :: thesis: verum

end;assume W .length() = 0 ; :: thesis: P

then W is V5() by GLIB_001:def 26;

hence P

S

proof

A13:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A5: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let W be DWalk of F_{1}(); :: thesis: ( W .length() = k + 1 implies P_{1}[W] )

assume A6: W .length() = k + 1 ; :: thesis: P_{1}[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: P_{1}[W .cut (1,L)]
by A5;

( W . (L + 1) in the_Edges_of F_{1}() & (the_Source_of F_{1}()) . (W . (L + 1)) = (W .cut (1,L)) .last() )

hence P_{1}[W]
by A2, A7, A9; :: thesis: verum

end;assume A5: S

let W be DWalk of F

assume A6: W .length() = k + 1 ; :: thesis: P

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: P

( W . (L + 1) in the_Edges_of F

proof

then
W . (L + 1) in ((W .cut (1,L)) .last()) .edgesOut()
by GLIB_000:58;
A10:
L + 0 < ((len W) - 2) + 2
by A7, XREAL_1:8;

then W . (L + 1) Joins W . L,W . (L + 2),F_{1}()
by GLIB_001:def 3;

hence W . (L + 1) in the_Edges_of F_{1}()
by GLIB_000:def 13; :: thesis: (the_Source_of F_{1}()) . (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 F_{1}()) . (W . (L + 1)) = (W .cut (1,L)) .last()
by A10, GLIB_001:def 25; :: thesis: verum

end;then W . (L + 1) Joins W . L,W . (L + 2),F

hence W . (L + 1) in the_Edges_of F

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 F

hence P

let W be DWalk of F

S

hence P