let G be _finite real-weighted WGraph; for EL being FF:ELabeling of G
for source being Vertex of G holds AP:CompSeq (EL,source) is halting
let EL be FF:ELabeling of G; for source being Vertex of G holds AP:CompSeq (EL,source) is halting
let source be Vertex of G; AP:CompSeq (EL,source) is halting
set CS = AP:CompSeq (EL,source);
now not for n being Nat holds (AP:CompSeq (EL,source)) . n <> (AP:CompSeq (EL,source)) . (n + 1)set x =
card (the_Vertices_of G);
defpred S1[
Nat]
means card (dom ((AP:CompSeq (EL,source)) . $1)) = $1
+ 1;
assume A1:
for
n being
Nat holds
(AP:CompSeq (EL,source)) . n <> (AP:CompSeq (EL,source)) . (n + 1)
;
contradictionA2:
now for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )set Gn =
(AP:CompSeq (EL,source)) . n;
set Gn1 =
(AP:CompSeq (EL,source)) . (n + 1);
set Next =
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
set e = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
A3:
(AP:CompSeq (EL,source)) . (n + 1) = AP:Step ((AP:CompSeq (EL,source)) . n)
by Def12;
assume A4:
S1[
n]
;
S1[n + 1]now S1[n + 1]per cases
( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) ) or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) ) )
;
suppose A5:
(
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & not
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) )
;
S1[n + 1]then
(AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))
by A3, Def10;
then
dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
by Lm1;
hence
S1[
n + 1]
by A4, A5, CARD_2:41;
verum end; suppose A6:
(
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} &
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) )
;
S1[n + 1]then
(AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))
by A3, Def10;
then A7:
dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))}
by Lm1;
( the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n or the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n )
by A6, Def9;
then
not
(the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n)
by A6;
hence
S1[
n + 1]
by A4, A7, CARD_2:41;
verum end; hence
S1[
n + 1]
;
verum end;
dom ((AP:CompSeq (EL,source)) . 0) = {source}
by Th4;
then A8:
S1[
0 ]
by CARD_1:30;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A8, A2);
then
card (dom ((AP:CompSeq (EL,source)) . (card (the_Vertices_of G)))) = (card (the_Vertices_of G)) + 1
;
then
1
+ (card (the_Vertices_of G)) <= (card (the_Vertices_of G)) + 0
by NAT_1:43;
hence
contradiction
by XREAL_1:6;
verum end;
hence
AP:CompSeq (EL,source) is halting
; verum