set S = (LexBFS:CSeq G) ``1 ;
set CS = LexBFS:CSeq G;
A1:
((LexBFS:CSeq G) ``1) .Lifespan() = (LexBFS:CSeq G) .Lifespan()
by Th39;
thus ((LexBFS:CSeq G) ``1) . 0 =
((LexBFS:CSeq G) . 0) `1
by Def15
.=
(LexBFS:Init G) `1
by Def16
.=
{}
; LEXBFS:def 9 ( (LexBFS:CSeq G) ``1 is iterative & (LexBFS:CSeq G) ``1 is halting & ((LexBFS:CSeq G) ``1) .Lifespan() = G .order() & ( for n being Nat st n < ((LexBFS:CSeq G) ``1) .Lifespan() holds
ex w being Vertex of G st
( not w in dom (((LexBFS:CSeq G) ``1) . n) & ((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n)) ) ) )
now for k, n being Nat st ((LexBFS:CSeq G) ``1) . k = ((LexBFS:CSeq G) ``1) . n holds
((LexBFS:CSeq G) ``1) . (k + 1) = ((LexBFS:CSeq G) ``1) . (n + 1)let k,
n be
Nat;
( ((LexBFS:CSeq G) ``1) . k = ((LexBFS:CSeq G) ``1) . n implies ((LexBFS:CSeq G) ``1) . (b1 + 1) = ((LexBFS:CSeq G) ``1) . (b2 + 1) )assume A2:
((LexBFS:CSeq G) ``1) . k = ((LexBFS:CSeq G) ``1) . n
;
((LexBFS:CSeq G) ``1) . (b1 + 1) = ((LexBFS:CSeq G) ``1) . (b2 + 1)A3:
((LexBFS:CSeq G) ``1) . (k + 1) = ((LexBFS:CSeq G) . (k + 1)) `1
by Def15;
A4:
((LexBFS:CSeq G) ``1) . k = ((LexBFS:CSeq G) . k) `1
by Def15;
A5:
((LexBFS:CSeq G) ``1) . (n + 1) = ((LexBFS:CSeq G) . (n + 1)) `1
by Def15;
A6:
((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) . n) `1
by Def15;
per cases
( ( k <= G .order() & n <= G .order() ) or ( k <= G .order() & n >= G .order() ) or ( k >= G .order() & n <= G .order() ) or ( k >= G .order() & n >= G .order() ) )
;
suppose A8:
(
k <= G .order() &
n >= G .order() )
;
((LexBFS:CSeq G) ``1) . (b1 + 1) = ((LexBFS:CSeq G) ``1) . (b2 + 1)then A9:
(LexBFS:CSeq G) . n = (LexBFS:CSeq G) . (G .order())
by Th33;
A10:
card (dom (((LexBFS:CSeq G) . (G .order())) `1)) = G .order()
by Th32;
A11:
n + 1
>= G .order()
by A8, NAT_1:13;
card (dom (((LexBFS:CSeq G) . k) `1)) = k
by A8, Th32;
then
k + 1
>= G .order()
by A2, A4, A6, A9, A10, NAT_1:13;
hence ((LexBFS:CSeq G) ``1) . (k + 1) =
((LexBFS:CSeq G) . (G .order())) `1
by A3, Th33
.=
((LexBFS:CSeq G) ``1) . (n + 1)
by A5, A11, Th33
;
verum end; suppose A12:
(
k >= G .order() &
n <= G .order() )
;
((LexBFS:CSeq G) ``1) . (b1 + 1) = ((LexBFS:CSeq G) ``1) . (b2 + 1)then A13:
(LexBFS:CSeq G) . k = (LexBFS:CSeq G) . (G .order())
by Th33;
A14:
card (dom (((LexBFS:CSeq G) . (G .order())) `1)) = G .order()
by Th32;
card (dom (((LexBFS:CSeq G) . n) `1)) = n
by A12, Th32;
then A15:
n + 1
>= G .order()
by A2, A4, A6, A13, A14, NAT_1:13;
k + 1
>= G .order()
by A12, NAT_1:13;
hence ((LexBFS:CSeq G) ``1) . (k + 1) =
((LexBFS:CSeq G) . (G .order())) `1
by A3, Th33
.=
((LexBFS:CSeq G) ``1) . (n + 1)
by A5, A15, Th33
;
verum end; end; end;
hence
(LexBFS:CSeq G) ``1 is iterative
; ( (LexBFS:CSeq G) ``1 is halting & ((LexBFS:CSeq G) ``1) .Lifespan() = G .order() & ( for n being Nat st n < ((LexBFS:CSeq G) ``1) .Lifespan() holds
ex w being Vertex of G st
( not w in dom (((LexBFS:CSeq G) ``1) . n) & ((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n)) ) ) )
(LexBFS:CSeq G) ``1 is eventually-constant
by Th38;
hence
(LexBFS:CSeq G) ``1 is halting
; ( ((LexBFS:CSeq G) ``1) .Lifespan() = G .order() & ( for n being Nat st n < ((LexBFS:CSeq G) ``1) .Lifespan() holds
ex w being Vertex of G st
( not w in dom (((LexBFS:CSeq G) ``1) . n) & ((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n)) ) ) )
A19:
(LexBFS:CSeq G) .Lifespan() = G .order()
by Th37;
hence
((LexBFS:CSeq G) ``1) .Lifespan() = G .order()
by Th39; for n being Nat st n < ((LexBFS:CSeq G) ``1) .Lifespan() holds
ex w being Vertex of G st
( not w in dom (((LexBFS:CSeq G) ``1) . n) & ((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n)) )
let n be Nat; ( n < ((LexBFS:CSeq G) ``1) .Lifespan() implies ex w being Vertex of G st
( not w in dom (((LexBFS:CSeq G) ``1) . n) & ((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n)) ) )
assume A20:
n < ((LexBFS:CSeq G) ``1) .Lifespan()
; ex w being Vertex of G st
( not w in dom (((LexBFS:CSeq G) ``1) . n) & ((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n)) )
A21:
n < G .order()
by A19, A20, Th39;
take w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n); ( not w in dom (((LexBFS:CSeq G) ``1) . n) & ((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n)) )
A22:
((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) . n) `1
by Def15;
A23:
card (dom (((LexBFS:CSeq G) . n) `1)) = n
by A21, Th32;
hence
not w in dom (((LexBFS:CSeq G) ``1) . n)
by A21, A22, Th30; ((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n))
((LexBFS:CSeq G) ``1) . (n + 1) = ((LexBFS:CSeq G) . (n + 1)) `1
by Def15;
hence
((LexBFS:CSeq G) ``1) . (n + 1) = (((LexBFS:CSeq G) ``1) . n) +* (w .--> ((((LexBFS:CSeq G) ``1) .Lifespan()) -' n))
by A1, A19, A20, A22, A23, Th31; verum