let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for source being Vertex of G
for i, j being Nat st i <= j holds
dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
let EL be FF:ELabeling of G; :: thesis: for source being Vertex of G
for i, j being Nat st i <= j holds
dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
let source be Vertex of G; :: thesis: for i, j being Nat st i <= j holds
dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
let i, j be Nat; :: thesis: ( i <= j implies dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j) )
set CS = AP:CompSeq (EL,source);
defpred S1[ Nat] means dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . (i + $1));
assume i <= j ; :: thesis: dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)
then consider k being Nat such that
A1: j = i + k by NAT_1:10;
A2: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set Gn = (AP:CompSeq (EL,source)) . (i + n);
set Gn1 = (AP:CompSeq (EL,source)) . (i + (n + 1));
set Next = AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n));
set e = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n));
(AP:CompSeq (EL,source)) . (i + (n + 1)) = (AP:CompSeq (EL,source)) . ((i + n) + 1) ;
then A3: (AP:CompSeq (EL,source)) . (i + (n + 1)) = AP:Step ((AP:CompSeq (EL,source)) . (i + n)) by Def12;
assume A4: S1[n] ; :: thesis: S1[n + 1]
now :: thesis: S1[n + 1]
per cases ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) = {} or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) in dom ((AP:CompSeq (EL,source)) . (i + n)) ) or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) in dom ((AP:CompSeq (EL,source)) . (i + n)) ) ) ;
suppose AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) = {} ; :: thesis: S1[n + 1]
hence S1[n + 1] by A4, A3, Def10; :: thesis: verum
end;
suppose ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) in dom ((AP:CompSeq (EL,source)) . (i + n)) ) ; :: thesis: S1[n + 1]
then (AP:CompSeq (EL,source)) . (i + (n + 1)) = ((AP:CompSeq (EL,source)) . (i + n)) +* (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n))) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n))) by A3, Def10;
then dom ((AP:CompSeq (EL,source)) . (i + n)) c= dom ((AP:CompSeq (EL,source)) . (i + (n + 1))) by FUNCT_4:10;
hence S1[n + 1] by A4, XBOOLE_1:1; :: thesis: verum
end;
suppose ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n)) in dom ((AP:CompSeq (EL,source)) . (i + n)) ) ; :: thesis: S1[n + 1]
then (AP:CompSeq (EL,source)) . (i + (n + 1)) = ((AP:CompSeq (EL,source)) . (i + n)) +* (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n))) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . (i + n))) by A3, Def10;
then dom ((AP:CompSeq (EL,source)) . (i + n)) c= dom ((AP:CompSeq (EL,source)) . (i + (n + 1))) by FUNCT_4:10;
hence S1[n + 1] by A4, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
hence S1[n + 1] ; :: thesis: verum
end;
A5: S1[ 0 ] ;
A6: for n being Nat holds S1[n] from NAT_1:sch 2(A5, A2);
 thus dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j) by A6, A1; :: thesis: verum