set V = {0,1};
set E = ;
set S = 0 .--> 0;
set T = 0 .--> 1;
A1: dom () = ;
A2: now :: thesis: for x being object st x in holds
() . x in {0,1}
let x be object ; :: thesis: ( x in implies () . x in {0,1} )
assume x in ; :: thesis: () . x in {0,1}
then x = 0 by TARSKI:def 1;
then (0 .--> 1) . x = 1 by FUNCOP_1:72;
hence (0 .--> 1) . x in {0,1} by TARSKI:def 2; :: thesis: verum
end;
A3: now :: thesis: for x being object st x in holds
() . x in {0,1}
let x be object ; :: thesis: ( x in implies () . x in {0,1} )
assume x in ; :: thesis: () . x in {0,1}
(0 .--> 0) . x = 0 ;
hence (0 .--> 0) . x in {0,1} by TARSKI:def 2; :: thesis: verum
end;
reconsider T = 0 .--> 1 as Function of ,{0,1} by ;
dom () = ;
then reconsider S = 0 .--> 0 as Function of ,{0,1} by ;
set G = createGraph ({0,1},,S,T);
A4: the_Edges_of (createGraph ({0,1},,S,T)) = by GLIB_000:6;
the_Target_of (createGraph ({0,1},,S,T)) = T by GLIB_000:6;
then A5: (the_Target_of (createGraph ({0,1},,S,T))) . 0 = 1 by FUNCOP_1:72;
the_Source_of (createGraph ({0,1},,S,T)) = S by GLIB_000:6;
then A6: (the_Source_of (createGraph ({0,1},,S,T))) . 0 = 0 ;
now :: thesis: for W being Walk of createGraph ({0,1},,S,T) holds not W is Cycle-like
given W being Walk of createGraph ({0,1},,S,T) such that A7: W is Cycle-like ; :: thesis: contradiction
per cases ( len W = 3 or len W <> 3 ) ;
suppose A8: len W = 3 ; :: thesis: contradiction
set e = W . (1 + 1);
set v1 = W . 1;
set v2 = W . (1 + 2);
A9: W . (1 + 1) Joins W . 1,W . (1 + 2), createGraph ({0,1},,S,T) by ;
W . 1 = W . (1 + 2) by ;
then A10: ( ( (the_Source_of (createGraph ({0,1},,S,T))) . (W . (1 + 1)) = W . 1 & (the_Target_of (createGraph ({0,1},,S,T))) . (W . (1 + 1)) = W . 1 ) or ( (the_Source_of (createGraph ({0,1},,S,T))) . (W . (1 + 1)) = W . 1 & (the_Target_of (createGraph ({0,1},,S,T))) . (W . (1 + 1)) = W . 1 ) ) by ;
W . (1 + 1) in the_Edges_of (createGraph ({0,1},,S,T)) by ;
then ( ( W . 1 = 0 & W . 1 = 1 ) or ( W . 1 = 1 & W . 1 = 0 ) ) by ;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
then A15: createGraph ({0,1},,S,T) is acyclic ;
set W1 = (createGraph ({0,1},,S,T)) .walkOf (0,0,1);
set W2 = ((createGraph ({0,1},,S,T)) .walkOf (0,0,1)) .reverse() ;
take createGraph ({0,1},,S,T) ; :: thesis: ( not createGraph ({0,1},,S,T) is trivial & createGraph ({0,1},,S,T) is finite & createGraph ({0,1},,S,T) is Tree-like )
A16: the_Vertices_of (createGraph ({0,1},,S,T)) = {0,1} by GLIB_000:6;
then reconsider a0 = 0 , a1 = 1 as Vertex of (createGraph ({0,1},,S,T)) by TARSKI:def 2;
now :: thesis: not card (the_Vertices_of (createGraph ({0,1},,S,T))) = 1end;
hence ( not createGraph ({0,1},,S,T) is trivial & createGraph ({0,1},,S,T) is finite ) by GLIB_000:def 19; :: thesis: createGraph ({0,1},,S,T) is Tree-like
0 in the_Edges_of (createGraph ({0,1},,S,T)) by ;
then 0 Joins 0 ,1, createGraph ({0,1},,S,T) by ;
then A17: (createGraph ({0,1},,S,T)) .walkOf (0,0,1) is_Walk_from 0 ,1 by GLIB_001:15;
then A18: ((createGraph ({0,1},,S,T)) .walkOf (0,0,1)) .reverse() is_Walk_from 1, 0 by GLIB_001:23;
now :: thesis: for u, v being Vertex of (createGraph ({0,1},,S,T)) ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v
let u, v be Vertex of (createGraph ({0,1},,S,T)); :: thesis: ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v
now :: thesis: ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v
per cases ( ( u = 0 & v = 0 ) or ( u = 0 & v = 1 ) or ( u = 1 & v = 0 ) or ( u = 1 & v = 1 ) ) by ;
suppose ( u = 0 & v = 0 ) ; :: thesis: ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v
end;
suppose ( u = 0 & v = 1 ) ; :: thesis: ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v
hence ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v by A17; :: thesis: verum
end;
suppose ( u = 1 & v = 0 ) ; :: thesis: ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v
hence ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v by A18; :: thesis: verum
end;
suppose ( u = 1 & v = 1 ) ; :: thesis: ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v
end;
end;
end;
hence ex W being Walk of createGraph ({0,1},,S,T) st W is_Walk_from u,v ; :: thesis: verum
end;
then createGraph ({0,1},,S,T) is connected ;
hence createGraph ({0,1},,S,T) is Tree-like by A15; :: thesis: verum