let G be _finite real-weighted WGraph; for EL being FF:ELabeling of G
for source being Vertex of G
for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
let EL be FF:ELabeling of G; for source being Vertex of G
for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
let source be Vertex of G; for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
let n be Nat; for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
let v be set ; ( v in dom ((AP:CompSeq (EL,source)) . n) implies ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v )
set SG = the_Source_of G;
set TG = the_Target_of G;
set CS = AP:CompSeq (EL,source);
set L = (AP:CompSeq (EL,source)) .Lifespan() ;
set GL = (AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan());
set GL1 = (AP:CompSeq (EL,source)) . (((AP:CompSeq (EL,source)) .Lifespan()) + 1);
defpred S1[ Nat] means for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . (n + $1)) . v;
defpred S2[ Nat] means (AP:CompSeq (EL,source)) . ((AP:CompSeq (EL,source)) .Lifespan()) = (AP:CompSeq (EL,source)) . (((AP:CompSeq (EL,source)) .Lifespan()) + $1);
A1:
AP:CompSeq (EL,source) is halting
by Th6;
A2:
now for k being Nat st S2[k] holds
S2[k + 1]end;
A3:
S2[ 0 ]
;
A4:
for k being Nat holds S2[k]
from NAT_1:sch 2(A3, A2);
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A5:
S1[
k]
;
S1[k + 1]set Gn =
(AP:CompSeq (EL,source)) . (n + k);
set Gn1 =
(AP:CompSeq (EL,source)) . ((n + k) + 1);
set Next =
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k));
set e = the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k));
A6:
(AP:CompSeq (EL,source)) . ((n + k) + 1) = AP:Step ((AP:CompSeq (EL,source)) . (n + k))
by Def12;
now S1[k + 1]per cases
( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) = {} or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) in dom ((AP:CompSeq (EL,source)) . (n + k)) ) or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) in dom ((AP:CompSeq (EL,source)) . (n + k)) ) )
;
suppose A7:
(
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) <> {} & not
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) in dom ((AP:CompSeq (EL,source)) . (n + k)) )
;
S1[k + 1]then A8:
(AP:CompSeq (EL,source)) . ((n + k) + 1) = ((AP:CompSeq (EL,source)) . (n + k)) +* (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k))) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)))
by A6, Def10;
now for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . vlet v be
set ;
( v in dom ((AP:CompSeq (EL,source)) . n) implies ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v )assume A9:
v in dom ((AP:CompSeq (EL,source)) . n)
;
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . vthen A10:
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . (n + k)) . v
by A5;
dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + k))
by Th5, NAT_1:11;
then
v <> (the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k))
by A7, A9;
hence
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v
by A8, A10, Lm4;
verum end; hence
S1[
k + 1]
;
verum end; suppose A11:
(
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) <> {} &
(the_Source_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) in dom ((AP:CompSeq (EL,source)) . (n + k)) )
;
S1[k + 1]then A12:
( the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) is_forward_edge_wrt (AP:CompSeq (EL,source)) . (n + k) or the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)) is_backward_edge_wrt (AP:CompSeq (EL,source)) . (n + k) )
by Def9;
A13:
(AP:CompSeq (EL,source)) . ((n + k) + 1) = ((AP:CompSeq (EL,source)) . (n + k)) +* (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k))) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k)))
by A6, A11, Def10;
now for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . vlet v be
set ;
( v in dom ((AP:CompSeq (EL,source)) . n) implies ((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v )assume A14:
v in dom ((AP:CompSeq (EL,source)) . n)
;
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . vthen A15:
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . (n + k)) . v
by A5;
dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + k))
by Th5, NAT_1:11;
then
v <> (the_Target_of G) . the
Element of
AP:NextBestEdges ((AP:CompSeq (EL,source)) . (n + k))
by A11, A12, A14;
hence
((AP:CompSeq (EL,source)) . n) . v = ((AP:CompSeq (EL,source)) . ((n + k) + 1)) . v
by A13, A15, Lm4;
verum end; hence
S1[
k + 1]
;
verum end; end; end; hence
S1[
k + 1]
;
verum end;
then A16:
for k being Nat st S1[k] holds
S1[k + 1]
;
A17:
S1[ 0 ]
;
A18:
for k being Nat holds S1[k]
from NAT_1:sch 2(A17, A16);
assume A19:
v in dom ((AP:CompSeq (EL,source)) . n)
; ((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
hence
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v
; verum