:: GRAPHSP semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: GRAPHSP:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for x being set holds
( ( not x in rng p & p is one-to-one ) iff p ^ <*x*> is one-to-one )
proof end;

theorem Th2: :: GRAPHSP:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for p being FinSequence of X
for ii being Integer st 1 <= ii & ii <= len p holds
p . ii in X
proof end;

theorem Th3: :: GRAPHSP:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for p being FinSequence of X
for ii being Integer st 1 <= ii & ii <= len p holds
p /. ii = p . ii
proof end;

theorem Th4: :: GRAPHSP:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for pe being FinSequence of the Edges of G
for W being Function st W is_weight_of G & len pe = 1 holds
cost pe,W = W . (pe . 1)
proof end;

theorem Th5: :: GRAPHSP:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for e being set st e in the Edges of G holds
<*e*> is oriented Simple Chain of G
proof end;

Lm1: for n being Nat
for p, q being FinSequence st 1 <= n & n <= len p holds
p . n = (p ^ q) . n
proof end;

Lm2: for n being Nat
for p, q being FinSequence st 1 <= n & n <= len q holds
q . n = (p ^ q) . ((len p) + n)
proof end;

theorem Th6: :: GRAPHSP:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for pe, qe being FinSequence of the Edges of G
for p being oriented Simple Chain of G st p = pe ^ qe & len pe >= 1 & len qe >= 1 holds
( the Target of G . (p . (len p)) <> the Target of G . (pe . (len pe)) & the Source of G . (p . 1) <> the Source of G . (qe . 1) )
proof end;

theorem Th7: :: GRAPHSP:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for p being oriented Chain of G
for V being set
for v1, v2 being Vertex of G holds
( p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2} )
proof end;

theorem Th8: :: GRAPHSP:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for p being oriented Chain of G
for W being Function
for V being set
for v1, v2 being Vertex of G holds
( p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/ {v2},W )
proof end;

theorem Th9: :: GRAPHSP:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for p, q being oriented Chain of G
for W being Function
for V being set
for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds
cost p,W = cost q,W
proof end;

theorem Th10: :: GRAPHSP:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being oriented Graph
for v1, v2 being Vertex of G
for e1, e2 being set st e1 in the Edges of G & e2 in the Edges of G & e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 holds
e1 = e2
proof end;

Lm3: for i being Nat
for G being Graph
for pe being FinSequence of the Edges of G st 1 <= i & i <= len pe holds
( the Source of G . (pe . i) in the Vertices of G & the Target of G . (pe . i) in the Vertices of G )
proof end;

theorem Th11: :: GRAPHSP:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for U, V being set
for v1, v2 being Vertex of G st the Vertices of G = U \/ V & v1 in U & v2 in V & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the Edges of G or not e orientedly_joins v3,v4 ) ) holds
for p being oriented Chain of G holds not p is_orientedpath_of v1,v2
proof end;

Lm4: for i being Nat
for G being Graph
for pe being FinSequence of the Edges of G
for v1 being Vertex of G st 1 <= i & i <= len pe & ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) holds
v1 in vertices pe
proof end;

theorem Th12: :: GRAPHSP:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for p being oriented Chain of G
for U, V being set
for v1, v2 being Vertex of G st the Vertices of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the Edges of G or not e orientedly_joins v3,v4 ) ) & p is_orientedpath_of v1,v2 holds
p is_orientedpath_of v1,v2,U
proof end;

theorem Th13: :: GRAPHSP:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for V being set
for G being finite Graph
for P, Q being oriented Chain of G
for v1, v2, v3 being Vertex of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of v1,v3,V,W & ( for e being set holds
( not e in the Edges of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
proof end;

theorem Th14: :: GRAPHSP:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for e being set
for G being oriented finite Graph
for P being oriented Chain of G
for W being Function of the Edges of G, Real>=0
for v1, v2 being Vertex of G st e in the Edges of G & v1 <> v2 & P = <*e*> & e orientedly_joins v1,v2 holds
P is_shortestpath_of v1,v2,{v1},W
proof end;

theorem Th15: :: GRAPHSP:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for e, V being set
for G being oriented finite Graph
for P, Q being oriented Chain of G
for W being Function of the Edges of G, Real>=0
for v1, v2, v3 being Vertex of G st e in the Edges of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the Edges of G or not ee orientedly_joins v4,v3 ) ) holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
proof end;

theorem Th16: :: GRAPHSP:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for U, V being set
for G being oriented finite Graph
for P being oriented Chain of G
for W being Function of the Edges of G, Real>=0
for v1, v2 being Vertex of G st the Vertices of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds
for e being set holds
( not e in the Edges of G or not e orientedly_joins v3,v4 ) ) holds
( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )
proof end;

notation
let f be Function;
let i, x be set ;
synonym f,i := x for f +* i,x;
end;

theorem Th17: :: GRAPHSP:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f being Function holds rng (f,x := y) c= (rng f) \/ {y}
proof end;

definition
let f be FinSequence of REAL ;
let x be set ;
let r be Real;
:: original: :=
redefine func f,x := r -> FinSequence of REAL ;
coherence
f,x := r is FinSequence of REAL
proof end;
end;

definition
let i, k be Nat;
let f be FinSequence of REAL ;
let r be Real;
func f,i := k,r -> FinSequence of REAL equals :: GRAPHSP:def 1
(f,i := k),k := r;
coherence
(f,i := k),k := r is FinSequence of REAL
;
end;

:: deftheorem defines := GRAPHSP:def 1 :
for i, k being Nat
for f being FinSequence of REAL
for r being Real holds f,i := k,r = (f,i := k),k := r;

theorem Th18: :: GRAPHSP:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k being Nat
for f being Element of REAL *
for r being Real st i <> k & i in dom f holds
(f,i := k,r) . i = k
proof end;

theorem Th19: :: GRAPHSP:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, i, k being Nat
for f being Element of REAL *
for r being Real st m <> i & m <> k & m in dom f holds
(f,i := k,r) . m = f . m
proof end;

theorem Th20: :: GRAPHSP:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i being Nat
for f being Element of REAL *
for r being Real st k in dom f holds
(f,i := k,r) . k = r
proof end;

theorem Th21: :: GRAPHSP:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k being Nat
for f being Element of REAL *
for r being Real holds dom (f,i := k,r) = dom f
proof end;

definition
let X be set ;
:: original: id
redefine func id X -> Element of Funcs X,X;
coherence
id X is Element of Funcs X,X
proof end;
end;

definition
let X be set ;
let f, g be Function of X,X;
:: original: *
redefine func g * f -> Function of X,X;
coherence
f * g is Function of X,X
proof end;
end;

definition
let X be set ;
let f, g be Element of Funcs X,X;
:: original: *
redefine func g * f -> Element of Funcs X,X;
coherence
f * g is Element of Funcs X,X
proof end;
end;

definition
let X be set ;
let f be Element of Funcs X,X;
let g be Element of X;
:: original: .
redefine func f . g -> Element of X;
coherence
f . g is Element of X
proof end;
end;

definition
let X be set ;
let f be Element of Funcs X,X;
func repeat f -> Function of NAT , Funcs X,X means :Def2: :: GRAPHSP:def 2
( it . 0 = id X & ( for i being Nat holds it . (i + 1) = f * (it . i) ) );
existence
ex b1 being Function of NAT , Funcs X,X st
( b1 . 0 = id X & ( for i being Nat holds b1 . (i + 1) = f * (b1 . i) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT , Funcs X,X st b1 . 0 = id X & ( for i being Nat holds b1 . (i + 1) = f * (b1 . i) ) & b2 . 0 = id X & ( for i being Nat holds b2 . (i + 1) = f * (b2 . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines repeat GRAPHSP:def 2 :
for X being set
for f being Element of Funcs X,X
for b3 being Function of NAT , Funcs X,X holds
( b3 = repeat f iff ( b3 . 0 = id X & ( for i being Nat holds b3 . (i + 1) = f * (b3 . i) ) ) );

theorem Th22: :: GRAPHSP:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of Funcs (REAL * ),(REAL * )
for f being Element of REAL *
for n, i being Nat holds ((repeat F) . 0) . f = f
proof end;

Lm5: for X being set
for f being Element of Funcs X,X holds dom f = X
proof end;

theorem Th23: :: GRAPHSP:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of Funcs (REAL * ),(REAL * )
for f being Element of REAL *
for i being Nat holds ((repeat (F * G)) . (i + 1)) . f = F . (G . (((repeat (F * G)) . i) . f))
proof end;

definition
let g be Element of Funcs (REAL * ),(REAL * );
let f be Element of REAL * ;
:: original: .
redefine func g . f -> Element of REAL * ;
coherence
g . f is Element of REAL *
proof end;
end;

definition
let f be Element of REAL * ;
let n be Nat;
func OuterVx f,n -> Subset of NAT equals :: GRAPHSP:def 3
{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } ;
coherence
{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } is Subset of NAT
proof end;
end;

:: deftheorem defines OuterVx GRAPHSP:def 3 :
for f being Element of REAL *
for n being Nat holds OuterVx f,n = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } ;

definition
let f be Element of Funcs (REAL * ),(REAL * );
let g be Element of REAL * ;
let n be Nat;
assume A1: ex i being Nat st OuterVx (((repeat f) . i) . g),n = {} ;
func LifeSpan f,g,n -> Nat means :Def4: :: GRAPHSP:def 4
( OuterVx (((repeat f) . it) . g),n = {} & ( for k being Nat st OuterVx (((repeat f) . k) . g),n = {} holds
it <= k ) );
existence
ex b1 being Nat st
( OuterVx (((repeat f) . b1) . g),n = {} & ( for k being Nat st OuterVx (((repeat f) . k) . g),n = {} holds
b1 <= k ) )
proof end;
uniqueness
for b1, b2 being Nat st OuterVx (((repeat f) . b1) . g),n = {} & ( for k being Nat st OuterVx (((repeat f) . k) . g),n = {} holds
b1 <= k ) & OuterVx (((repeat f) . b2) . g),n = {} & ( for k being Nat st OuterVx (((repeat f) . k) . g),n = {} holds
b2 <= k ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines LifeSpan GRAPHSP:def 4 :
for f being Element of Funcs (REAL * ),(REAL * )
for g being Element of REAL *
for n being Nat st ex i being Nat st OuterVx (((repeat f) . i) . g),n = {} holds
for b4 being Nat holds
( b4 = LifeSpan f,g,n iff ( OuterVx (((repeat f) . b4) . g),n = {} & ( for k being Nat st OuterVx (((repeat f) . k) . g),n = {} holds
b4 <= k ) ) );

definition
let f be Element of Funcs (REAL * ),(REAL * );
let n be Nat;
func while_do f,n -> Element of Funcs (REAL * ),(REAL * ) means :Def5: :: GRAPHSP:def 5
( dom it = REAL * & ( for h being Element of REAL * holds it . h = ((repeat f) . (LifeSpan f,h,n)) . h ) );
existence
ex b1 being Element of Funcs (REAL * ),(REAL * ) st
( dom b1 = REAL * & ( for h being Element of REAL * holds b1 . h = ((repeat f) . (LifeSpan f,h,n)) . h ) )
proof end;
uniqueness
for b1, b2 being Element of Funcs (REAL * ),(REAL * ) st dom b1 = REAL * & ( for h being Element of REAL * holds b1 . h = ((repeat f) . (LifeSpan f,h,n)) . h ) & dom b2 = REAL * & ( for h being Element of REAL * holds b2 . h = ((repeat f) . (LifeSpan f,h,n)) . h ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines while_do GRAPHSP:def 5 :
for f being Element of Funcs (REAL * ),(REAL * )
for n being Nat
for b3 being Element of Funcs (REAL * ),(REAL * ) holds
( b3 = while_do f,n iff ( dom b3 = REAL * & ( for h being Element of REAL * holds b3 . h = ((repeat f) . (LifeSpan f,h,n)) . h ) ) );

definition
let G be oriented Graph;
let v1, v2 be Vertex of G;
assume A1: ex e being set st
( e in the Edges of G & e orientedly_joins v1,v2 ) ;
func Edge v1,v2 -> set means :Def6: :: GRAPHSP:def 6
ex e being set st
( it = e & e in the Edges of G & e orientedly_joins v1,v2 );
existence
ex b1 being set ex e being set st
( b1 = e & e in the Edges of G & e orientedly_joins v1,v2 )
by A1;
uniqueness
for b1, b2 being set st ex e being set st
( b1 = e & e in the Edges of G & e orientedly_joins v1,v2 ) & ex e being set st
( b2 = e & e in the Edges of G & e orientedly_joins v1,v2 ) holds
b1 = b2
by Th10;
end;

:: deftheorem Def6 defines Edge GRAPHSP:def 6 :
for G being oriented Graph
for v1, v2 being Vertex of G st ex e being set st
( e in the Edges of G & e orientedly_joins v1,v2 ) holds
for b4 being set holds
( b4 = Edge v1,v2 iff ex e being set st
( b4 = e & e in the Edges of G & e orientedly_joins v1,v2 ) );

definition
let G be oriented Graph;
let v1, v2 be Vertex of G;
let W be Function;
func Weight v1,v2,W -> set equals :Def7: :: GRAPHSP:def 7
W . (Edge v1,v2) if ex e being set st
( e in the Edges of G & e orientedly_joins v1,v2 )
otherwise - 1;
correctness
coherence
( ( ex e being set st
( e in the Edges of G & e orientedly_joins v1,v2 ) implies W . (Edge v1,v2) is set ) & ( ( for e being set holds
( not e in the Edges of G or not e orientedly_joins v1,v2 ) ) implies - 1 is set ) )
;
consistency
for b1 being set holds verum
;
;
end;

:: deftheorem Def7 defines Weight GRAPHSP:def 7 :
for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function holds
( ( ex e being set st
( e in the Edges of G & e orientedly_joins v1,v2 ) implies Weight v1,v2,W = W . (Edge v1,v2) ) & ( ( for e being set holds
( not e in the Edges of G or not e orientedly_joins v1,v2 ) ) implies Weight v1,v2,W = - 1 ) );

definition
let G be oriented Graph;
let v1, v2 be Vertex of G;
let W be Function of the Edges of G, Real>=0 ;
:: original: Weight
redefine func Weight v1,v2,W -> Real;
coherence
Weight v1,v2,W is Real
proof end;
end;

theorem Th24: :: GRAPHSP:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function of the Edges of G, Real>=0 holds
( Weight v1,v2,W >= 0 iff ex e being set st
( e in the Edges of G & e orientedly_joins v1,v2 ) )
proof end;

theorem :: GRAPHSP:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function of the Edges of G, Real>=0 holds
( Weight v1,v2,W = - 1 iff for e being set holds
( not e in the Edges of G or not e orientedly_joins v1,v2 ) ) by Def7, Th24;

theorem Th26: :: GRAPHSP:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for e being set
for G being oriented Graph
for v1, v2 being Vertex of G
for W being Function of the Edges of G, Real>=0 st e in the Edges of G & e orientedly_joins v1,v2 holds
Weight v1,v2,W = W . e
proof end;

definition
let f be Element of REAL * ;
let n be Nat;
func UnusedVx f,n -> Subset of NAT equals :: GRAPHSP:def 8
{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ;
coherence
{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } is Subset of NAT
proof end;
end;

:: deftheorem defines UnusedVx GRAPHSP:def 8 :
for f being Element of REAL *
for n being Nat holds UnusedVx f,n = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ;

definition
let f be Element of REAL * ;
let n be Nat;
func UsedVx f,n -> Subset of NAT equals :: GRAPHSP:def 9
{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } ;
coherence
{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } is Subset of NAT
proof end;
end;

:: deftheorem defines UsedVx GRAPHSP:def 9 :
for f being Element of REAL *
for n being Nat holds UsedVx f,n = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } ;

theorem Th27: :: GRAPHSP:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * holds UnusedVx f,n c= Seg n
proof end;

registration
let f be Element of REAL * ;
let n be Nat;
cluster UnusedVx f,n -> finite ;
coherence
UnusedVx f,n is finite
proof end;
end;

theorem Th28: :: GRAPHSP:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * holds OuterVx f,n c= UnusedVx f,n
proof end;

theorem Th29: :: GRAPHSP:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * holds OuterVx f,n c= Seg n
proof end;

registration
let f be Element of REAL * ;
let n be Nat;
cluster OuterVx f,n -> finite ;
coherence
OuterVx f,n is finite
proof end;
end;

definition
let X be finite Subset of NAT ;
let f be Element of REAL * ;
let n be Nat;
func Argmin X,f,n -> Nat means :Def10: :: GRAPHSP:def 10
( ( X <> {} implies ex i being Nat st
( i = it & i in X & ( for k being Nat st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies it = 0 ) );
existence
ex b1 being Nat st
( ( X <> {} implies ex i being Nat st
( i = b1 & i in X & ( for k being Nat st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Nat st ( X <> {} implies ex i being Nat st
( i = b1 & i in X & ( for k being Nat st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies b1 = 0 ) & ( X <> {} implies ex i being Nat st
( i = b2 & i in X & ( for k being Nat st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies b2 = 0 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines Argmin GRAPHSP:def 10 :
for X being finite Subset of NAT
for f being Element of REAL *
for n, b4 being Nat holds
( b4 = Argmin X,f,n iff ( ( X <> {} implies ex i being Nat st
( i = b4 & i in X & ( for k being Nat st k in X holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) ) & ( X = {} implies b4 = 0 ) ) );

theorem Th30: :: GRAPHSP:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, j being Nat
for f being Element of REAL * st OuterVx f,n <> {} & j = Argmin (OuterVx f,n),f,n holds
( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 )
proof end;

theorem Th31: :: GRAPHSP:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * holds Argmin (OuterVx f,n),f,n <= n
proof end;

definition
let n be Nat;
func findmin n -> Element of Funcs (REAL * ),(REAL * ) means :Def11: :: GRAPHSP:def 11
( dom it = REAL * & ( for f being Element of REAL * holds it . f = f,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx f,n),f,n),(- 1) ) );
existence
ex b1 being Element of Funcs (REAL * ),(REAL * ) st
( dom b1 = REAL * & ( for f being Element of REAL * holds b1 . f = f,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx f,n),f,n),(- 1) ) )
proof end;
uniqueness
for b1, b2 being Element of Funcs (REAL * ),(REAL * ) st dom b1 = REAL * & ( for f being Element of REAL * holds b1 . f = f,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx f,n),f,n),(- 1) ) & dom b2 = REAL * & ( for f being Element of REAL * holds b2 . f = f,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx f,n),f,n),(- 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines findmin GRAPHSP:def 11 :
for n being Nat
for b2 being Element of Funcs (REAL * ),(REAL * ) holds
( b2 = findmin n iff ( dom b2 = REAL * & ( for f being Element of REAL * holds b2 . f = f,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx f,n),f,n),(- 1) ) ) );

theorem Th32: :: GRAPHSP:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for f being Element of REAL * st i in dom f & i > n & i <> ((n * n) + (3 * n)) + 1 holds
((findmin n) . f) . i = f . i
proof end;

theorem Th33: :: GRAPHSP:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for f being Element of REAL * st i in dom f & f . i = - 1 & i <> ((n * n) + (3 * n)) + 1 holds
((findmin n) . f) . i = - 1
proof end;

theorem Th34: :: GRAPHSP:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * holds dom ((findmin n) . f) = dom f
proof end;

Lm6: for k, n being Nat st k >= 1 holds
n <= k * n
proof end;

Lm7: for n being Nat holds
( 3 * n < ((n * n) + (3 * n)) + 1 & n < ((n * n) + (3 * n)) + 1 & 2 * n < ((n * n) + (3 * n)) + 1 )
proof end;

Lm8: for n, k being Nat holds
( ( n < k & k <= 2 * n implies ( ( not 2 * n < k or not k <= 3 * n ) & not k <= n & not k > 3 * n ) ) & ( ( k <= n or k > 3 * n ) implies ( ( not 2 * n < k or not k <= 3 * n ) & ( not n < k or not k <= 2 * n ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( not n < k or not k <= 2 * n ) & not k <= n & not k > 3 * n ) ) )
proof end;

theorem Th35: :: GRAPHSP:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * st OuterVx f,n <> {} holds
ex j being Nat st
( j in OuterVx f,n & 1 <= j & j <= n & ((findmin n) . f) . j = - 1 )
proof end;

definition
let f be Element of REAL * ;
let n, k be Nat;
func newpathcost f,n,k -> Real equals :: GRAPHSP:def 12
(f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));
correctness
coherence
(f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k)) is Real
;
;
end;

:: deftheorem defines newpathcost GRAPHSP:def 12 :
for f being Element of REAL *
for n, k being Nat holds newpathcost f,n,k = (f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));

definition
let n, k be Nat;
let f be Element of REAL * ;
pred f hasBetterPathAt n,k means :Def13: :: GRAPHSP:def 13
( ( f . (n + k) = - 1 or f /. ((2 * n) + k) > newpathcost f,n,k ) & f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k) >= 0 & f . k <> - 1 );
end;

:: deftheorem Def13 defines hasBetterPathAt GRAPHSP:def 13 :
for n, k being Nat
for f being Element of REAL * holds
( f hasBetterPathAt n,k iff ( ( f . (n + k) = - 1 or f /. ((2 * n) + k) > newpathcost f,n,k ) & f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k) >= 0 & f . k <> - 1 ) );

definition
let f be Element of REAL * ;
let n be Nat;
func Relax f,n -> Element of REAL * means :Def14: :: GRAPHSP:def 14
( dom it = dom f & ( for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies it . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies it . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies it . k = newpathcost f,n,(k -' (2 * n)) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies it . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies it . k = f . k ) ) ) );
existence
ex b1 being Element of REAL * st
( dom b1 = dom f & ( for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b1 . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b1 . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b1 . k = newpathcost f,n,(k -' (2 * n)) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b1 . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b1 . k = f . k ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of REAL * st dom b1 = dom f & ( for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b1 . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b1 . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b1 . k = newpathcost f,n,(k -' (2 * n)) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b1 . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b1 . k = f . k ) ) ) & dom b2 = dom f & ( for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b2 . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b2 . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b2 . k = newpathcost f,n,(k -' (2 * n)) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b2 . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b2 . k = f . k ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines Relax GRAPHSP:def 14 :
for f being Element of REAL *
for n being Nat
for b3 being Element of REAL * holds
( b3 = Relax f,n iff ( dom b3 = dom f & ( for k being Nat st k in dom f holds
( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b3 . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b3 . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b3 . k = newpathcost f,n,(k -' (2 * n)) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b3 . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b3 . k = f . k ) ) ) ) );

definition
let n be Nat;
func Relax n -> Element of Funcs (REAL * ),(REAL * ) means :Def15: :: GRAPHSP:def 15
( dom it = REAL * & ( for f being Element of REAL * holds it . f = Relax f,n ) );
existence
ex b1 being Element of Funcs (REAL * ),(REAL * ) st
( dom b1 = REAL * & ( for f being Element of REAL * holds b1 . f = Relax f,n ) )
proof end;
uniqueness
for b1, b2 being Element of Funcs (REAL * ),(REAL * ) st dom b1 = REAL * & ( for f being Element of REAL * holds b1 . f = Relax f,n ) & dom b2 = REAL * & ( for f being Element of REAL * holds b2 . f = Relax f,n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines Relax GRAPHSP:def 15 :
for n being Nat
for b2 being Element of Funcs (REAL * ),(REAL * ) holds
( b2 = Relax n iff ( dom b2 = REAL * & ( for f being Element of REAL * holds b2 . f = Relax f,n ) ) );

theorem Th36: :: GRAPHSP:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * holds dom ((Relax n) . f) = dom f
proof end;

theorem Th37: :: GRAPHSP:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for f being Element of REAL * st ( i <= n or i > 3 * n ) & i in dom f holds
((Relax n) . f) . i = f . i
proof end;

theorem Th38: :: GRAPHSP:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for f being Element of REAL * holds dom (((repeat ((Relax n) * (findmin n))) . i) . f) = dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f)
proof end;

theorem Th39: :: GRAPHSP:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for f being Element of REAL * st OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n <> {} holds
UnusedVx (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n c< UnusedVx (((repeat ((Relax n) * (findmin n))) . i) . f),n
proof end;

theorem Th40: :: GRAPHSP:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i, k being Nat
for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . i) . f & h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f & k = Argmin (OuterVx g,n),g,n & OuterVx g,n <> {} holds
( UsedVx h,n = (UsedVx g,n) \/ {k} & not k in UsedVx g,n )
proof end;

theorem Th41: :: GRAPHSP:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * ex i being Nat st
( i <= n & OuterVx (((repeat ((Relax n) * (findmin n))) . i) . f),n = {} )
proof end;

Lm9: for n, k being Nat holds n - k <= n
proof end;

Lm10: for p, q being FinSequence of NAT
for f being Element of REAL *
for i, n being Nat st ( for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . ((p /. (((len p) - k) + 1)) + n) ) & ( for k being Nat st 1 <= k & k < len q holds
q . ((len q) - k) = f . ((q /. (((len q) - k) + 1)) + n) ) & len p <= len q & p . (len p) = q . (len q) holds
for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = q . ((len q) - k)
proof end;

theorem Th42: :: GRAPHSP:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for f being Element of REAL * holds dom f = dom (((repeat ((Relax n) * (findmin n))) . i) . f)
proof end;

definition
let f, g be Element of REAL * ;
let m, n be Nat;
pred f,g equal_at m,n means :Def16: :: GRAPHSP:def 16
( dom f = dom g & ( for k being Nat st k in dom f & m <= k & k <= n holds
f . k = g . k ) );
end;

:: deftheorem Def16 defines equal_at GRAPHSP:def 16 :
for f, g being Element of REAL *
for m, n being Nat holds
( f,g equal_at m,n iff ( dom f = dom g & ( for k being Nat st k in dom f & m <= k & k <= n holds
f . k = g . k ) ) );

theorem Th43: :: GRAPHSP:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat
for f being Element of REAL * holds f,f equal_at m,n
proof end;

theorem Th44: :: GRAPHSP:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat
for f, g, h being Element of REAL * st f,g equal_at m,n & g,h equal_at m,n holds
f,h equal_at m,n
proof end;

theorem Th45: :: GRAPHSP:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for f being Element of REAL * holds ((repeat ((Relax n) * (findmin n))) . i) . f,((repeat ((Relax n) * (findmin n))) . (i + 1)) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
proof end;

theorem :: GRAPHSP:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of Funcs (REAL * ),(REAL * )
for f being Element of REAL *
for n, i being Nat st i < LifeSpan F,f,n holds
OuterVx (((repeat F) . i) . f),n <> {} by Def4;

theorem Th47: :: GRAPHSP:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for f being Element of REAL * holds f,((repeat ((Relax n) * (findmin n))) . i) . f equal_at (3 * n) + 1,(n * n) + (3 * n)
proof end;

theorem Th48: :: GRAPHSP:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for f being Element of REAL * st 1 <= n & 1 in dom f & f . (n + 1) <> - 1 & ( for i being Nat st 1 <= i & i <= n holds
f . i = 1 ) & ( for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ) holds
( 1 = Argmin (OuterVx f,n),f,n & UsedVx f,n = {} & {1} = UsedVx (((repeat ((Relax n) * (findmin n))) . 1) . f),n )
proof end;

theorem Th49: :: GRAPHSP:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i, m being Nat
for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . 1) . f & h = ((repeat ((Relax n) * (findmin n))) . i) . f & 1 <= i & i <= LifeSpan ((Relax n) * (findmin n)),f,n & m in UsedVx g,n holds
m in UsedVx h,n
proof end;

definition
let p be FinSequence of NAT ;
let f be Element of REAL * ;
let i, n be Nat;
pred p is_vertex_seq_at f,i,n means :Def17: :: GRAPHSP:def 17
( p . (len p) = i & ( for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . (n + (p /. (((len p) - k) + 1))) ) );
end;

:: deftheorem Def17 defines is_vertex_seq_at GRAPHSP:def 17 :
for p being FinSequence of NAT
for f being Element of REAL *
for i, n being Nat holds
( p is_vertex_seq_at f,i,n iff ( p . (len p) = i & ( for k being Nat st 1 <= k & k < len p holds
p . ((len p) - k) = f . (n + (p /. (((len p) - k) + 1))) ) ) );

definition
let p be FinSequence of NAT ;
let f be Element of REAL * ;
let i, n be Nat;
pred p is_simple_vertex_seq_at f,i,n means :Def18: :: GRAPHSP:def 18
( p . 1 = 1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one );
end;

:: deftheorem Def18 defines is_simple_vertex_seq_at GRAPHSP:def 18 :
for p being FinSequence of NAT
for f being Element of REAL *
for i, n being Nat holds
( p is_simple_vertex_seq_at f,i,n iff ( p . 1 = 1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one ) );

theorem :: GRAPHSP:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence of NAT
for f being Element of REAL *
for i, n being Nat st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n holds
p = q
proof end;

definition
let G be Graph;
let p be FinSequence of the Edges of G;
let vs be FinSequence;
pred p is_oriented_edge_seq_of vs means :Def19: :: GRAPHSP:def 19
( len vs = (len p) + 1 & ( for n being Nat st 1 <= n & n <= len p holds
( the Source of G . (p . n) = vs . n & the Target of G . (p . n) = vs . (n + 1) ) ) );
end;

:: deftheorem Def19 defines is_oriented_edge_seq_of GRAPHSP:def 19 :
for G being Graph
for p being FinSequence of the Edges of G
for vs being FinSequence holds
( p is_oriented_edge_seq_of vs iff ( len vs = (len p) + 1 & ( for n being Nat st 1 <= n & n <= len p holds
( the Source of G . (p . n) = vs . n & the Target of G . (p . n) = vs . (n + 1) ) ) ) );

theorem :: GRAPHSP:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being oriented Graph
for vs being FinSequence
for p, q being oriented Chain of G st p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs holds
p = q
proof end;

theorem :: GRAPHSP:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs1, vs2 being FinSequence
for p being oriented Chain of G st p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & len p >= 1 holds
vs1 = vs2
proof end;

Lm11: for i, n being Nat st 1 <= i & i <= n holds
( 1 < (2 * n) + i & (2 * n) + i < ((n * n) + (3 * n)) + 1 & i < (2 * n) + i )
proof end;

Lm12: for i, n being Nat st 1 <= i & i <= n holds
( 1 < n + i & n + i <= 2 * n & n + i < ((n * n) + (3 * n)) + 1 )
proof end;

Lm13: for i, n, j being Nat st 1 <= i & i <= n & j <= n holds
( 1 < ((2 * n) + (n * i)) + j & i < ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 )
proof end;

Lm14: for i, n, j being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds
( (3 * n) + 1 <= ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) )
proof end;

definition
let f be Element of REAL * ;
let G be oriented Graph;
let n be Nat;
let W be Function of the Edges of G, Real>=0 ;
pred f is_Input_of_Dijkstra_Alg G,n,W means :Def20: :: GRAPHSP:def 20
( len f = ((n * n) + (3 * n)) + 1 & Seg n = the Vertices of G & ( for i being Nat st 1 <= i & i <= n holds
( f . i = 1 & f . ((2 * n) + i) = 0 ) ) & f . (n + 1) = 0 & ( for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ) & ( for i, j being Vertex of G
for k, m being Nat st k = i & m = j holds
f . (((2 * n) + (n * k)) + m) = Weight i,j,W ) );
end;

:: deftheorem Def20 defines is_Input_of_Dijkstra_Alg GRAPHSP:def 20 :
for f being Element of REAL *
for G being oriented Graph
for n being Nat
for W being Function of the Edges of G, Real>=0 holds
( f is_Input_of_Dijkstra_Alg G,n,W iff ( len f = ((n * n) + (3 * n)) + 1 & Seg n = the Vertices of G & ( for i being Nat st 1 <= i & i <= n holds
( f . i = 1 & f . ((2 * n) + i) = 0 ) ) & f . (n + 1) = 0 & ( for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ) & ( for i, j being Vertex of G
for k, m being Nat st k = i & m = j holds
f . (((2 * n) + (n * k)) + m) = Weight i,j,W ) ) );

definition
let n be Nat;
func DijkstraAlgorithm n -> Element of Funcs (REAL * ),(REAL * ) equals :: GRAPHSP:def 21
while_do ((Relax n) * (findmin n)),n;
coherence
while_do ((Relax n) * (findmin n)),n is Element of Funcs (REAL * ),(REAL * )
;
end;

:: deftheorem defines DijkstraAlgorithm GRAPHSP:def 21 :
for n being Nat holds DijkstraAlgorithm n = while_do ((Relax n) * (findmin n)),n;

Lm15: for n being Nat
for f, h being Element of REAL *
for G being oriented finite Graph
for W being Function of the Edges of G, Real>=0
for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & h = ((repeat ((Relax n) * (findmin n))) . 1) . f holds
( ( for v3 being Vertex of G
for j being Nat st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Nat st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx h,n holds
h . (n + m) <> - 1 ) )
proof end;

Lm16: for n, k, i being Nat
for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & i in UsedVx g,n & len f = ((n * n) + (3 * n)) + 1 holds
h . (n + i) = g . (n + i)
proof end;

Lm17: for n, k, j being Nat
for g, f, h being Element of REAL *
for p being FinSequence of NAT st g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & len f = ((n * n) + (3 * n)) + 1 & p is_simple_vertex_seq_at g,j,n & g . (n + j) = h . (n + j) & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx g,n ) holds
p is_simple_vertex_seq_at h,j,n
proof end;

Lm18: for n, k, m, j being Nat
for g, f, h being Element of REAL *
for p being FinSequence of NAT st g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & len f = ((n * n) + (3 * n)) + 1 & p is_simple_vertex_seq_at g,m,n & m = h . (n + j) & g . (n + m) = h . (n + m) & m <> j & not j in UsedVx g,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx g,n ) holds
p ^ <*j*> is_simple_vertex_seq_at h,j,n
proof end;

Lm19: for n, i being Nat
for V being set
for f, g being Element of REAL *
for G being oriented finite Graph
for P being oriented Chain of G
for W being Function of the Edges of G, Real>=0
for v2, v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of v1,v2,V,W & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds
f . (((2 * n) + (n * m)) + j) = - 1 ) holds
g . (n + i) <> - 1
proof end;

Lm20: for n, k being Nat
for f, g, h being Element of REAL *
for G being oriented finite Graph
for W being Function of the Edges of G, Real>=0
for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx g,n <> {} & k >= 1 & 1 in UsedVx g,n & ( for v3 being Vertex of G
for j being Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx g,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx g,n,W & cost P,W = g . ((2 * n) + j) & ( not v3 in UsedVx g,n implies P islongestInShortestpath UsedVx g,n,v1,W ) ) ) & ( for m, j being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx g,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx g,n holds
g . (n + m) <> - 1 ) holds
( ( for v3 being Vertex of G
for j being Nat st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds
ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at h,j,n & ( for i being Nat st 1 <= i & i < len p holds
p . i in UsedVx h,n ) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v3, UsedVx h,n,W & cost P,W = h . ((2 * n) + j) & ( not v3 in UsedVx h,n implies P islongestInShortestpath UsedVx h,n,v1,W ) ) ) & ( for m, j being Nat st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx h,n holds
f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx h,n holds
h . (n + m) <> - 1 ) )
proof end;

theorem :: GRAPHSP:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, i being Nat
for f, g being Element of REAL *
for G being oriented finite Graph
for W being Function of the Edges of G, Real>=0
for v1, v2 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & 1 <> v2 & v2 = i & n >= 1 & g = (DijkstraAlgorithm n) . f holds
( the Vertices of G = (UsedVx g,n) \/ (UnusedVx g,n) & ( v2 in UsedVx g,n implies ex p being FinSequence of NAT ex P being oriented Chain of G st
( p is_simple_vertex_seq_at g,i,n & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v2,W & cost P,W = g . ((2 * n) + i) ) ) & ( v2 in UnusedVx g,n implies for Q being oriented Chain of G holds not Q is_orientedpath_of v1,v2 ) )
proof end;