defpred S1[ Nat] means for W being Walk of F1() st W .length() = \$1 holds
P1[W];
A3: S1[ 0 ]
proof
let W be Walk of F1(); :: thesis: ( W .length() = 0 implies P1[W] )
assume W .length() = 0 ; :: thesis: P1[W]
then W is V5() by GLIB_001:def 26;
hence P1[W] by A1; :: thesis: verum
end;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: S1[k] ; :: thesis: S1[k + 1]
let W be Walk of F1(); :: thesis: ( W .length() = k + 1 implies P1[W] )
assume A6: W .length() = k + 1 ; :: thesis: 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 ;
set W0 = W .cut (1,L);
A8: L + 0 <= ((len W) - 2) + 2 by ;
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 * ()) + 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() or (the_Target_of F1()) . (W . (L + 1)) = (W .cut (1,L)) .last() ) )
proof
L + 0 < ((len W) - 2) + 2 by ;
then A10: W . (L + 1) Joins W . L,W . (L + 2),F1() by GLIB_001:def 3;
A11: L = len (W .cut (1,L)) by ;
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 ;
then W . L = (W .cut (1,L)) .last() by ;
hence ( W . (L + 1) in the_Edges_of F1() & ( (the_Source_of F1()) . (W . (L + 1)) = (W .cut (1,L)) .last() or (the_Target_of F1()) . (W . (L + 1)) = (W .cut (1,L)) .last() ) ) by ; :: thesis: verum
end;
then W . (L + 1) in ((W .cut (1,L)) .last()) .edgesInOut() by GLIB_000:61;
hence P1[W] by A2, A7, A9; :: thesis: verum
end;
A13: for k being Nat holds S1[k] from NAT_1:sch 2(A3, A4);
let W be Walk of F1(); :: thesis: P1[W]
S1[W .length() ] by A13;
hence P1[W] ; :: thesis: verum