:: GRAPHSP semantic presentation

theorem Th1: :: GRAPHSP:1

for b₁ being FinSequence
for b₂ being set holds
( ( not b₂ in rng b₁ & b₁ is one-to-one ) iff b₁ ^ <*b₂*> is one-to-one )

proof end;

theorem Th2: :: GRAPHSP:2

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being Integer st 1 <= b₃ & b₃ <= len b₂ holds
b₂ . b₃ in b₁

proof end;

theorem Th3: :: GRAPHSP:3

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being Integer st 1 <= b₃ & b₃ <= len b₂ holds
b₂ /. b₃ = b₂ . b₃

proof end;

theorem Th4: :: GRAPHSP:4

for b₁ being Graph
for b₂ being FinSequence of the Edges of b₁
for b₃ being Function st b₃ is_weight_of b₁ & len b₂ = 1 holds
cost b₂,b₃ = b₃ . (b₂ . 1)

proof end;

theorem Th5: :: GRAPHSP:5

for b₁ being Graph
for b₂ being set st b₂ in the Edges of b₁ holds
<*b₂*> is oriented Simple Chain of b₁

proof end;

Lemma6: for b₁ being Nat
for b₂, b₃ being FinSequence st 1 <= b₁ & b₁ <= len b₂ holds
b₂ . b₁ = (b₂ ^ b₃) . b₁

proof end;

Lemma7: for b₁ being Nat
for b₂, b₃ being FinSequence st 1 <= b₁ & b₁ <= len b₃ holds
b₃ . b₁ = (b₂ ^ b₃) . ((len b₂) + b₁)

proof end;

theorem Th6: :: GRAPHSP:6

for b₁ being Graph
for b₂, b₃ being FinSequence of the Edges of b₁
for b₄ being oriented Simple Chain of b₁ st b₄ = b₂ ^ b₃ & len b₂ >= 1 & len b₃ >= 1 holds
( the Target of b₁ . (b₄ . (len b₄)) <> the Target of b₁ . (b₂ . (len b₂)) & the Source of b₁ . (b₄ . 1) <> the Source of b₁ . (b₃ . 1) )

proof end;

theorem Th7: :: GRAPHSP:7

for b₁ being Graph
for b₂ being oriented Chain of b₁
for b₃ being set
for b₄, b₅ being Vertex of b₁ holds
( b₂ is_orientedpath_of b₄,b₅,b₃ iff b₂ is_orientedpath_of b₄,b₅,b₃ \/ {b₅} )

proof end;

theorem Th8: :: GRAPHSP:8

for b₁ being Graph
for b₂ being oriented Chain of b₁
for b₃ being Function
for b₄ being set
for b₅, b₆ being Vertex of b₁ holds
( b₂ is_shortestpath_of b₅,b₆,b₄,b₃ iff b₂ is_shortestpath_of b₅,b₆,b₄ \/ {b₆},b₃ )

proof end;

theorem Th9: :: GRAPHSP:9

for b₁ being Graph
for b₂, b₃ being oriented Chain of b₁
for b₄ being Function
for b₅ being set
for b₆, b₇ being Vertex of b₁ st b₂ is_shortestpath_of b₆,b₇,b₅,b₄ & b₃ is_shortestpath_of b₆,b₇,b₅,b₄ holds
cost b₂,b₄ = cost b₃,b₄

proof end;

theorem Th10: :: GRAPHSP:10

for b₁ being oriented Graph
for b₂, b₃ being Vertex of b₁
for b₄, b₅ being set st b₄ in the Edges of b₁ & b₅ in the Edges of b₁ & b₄ orientedly_joins b₂,b₃ & b₅ orientedly_joins b₂,b₃ holds
b₄ = b₅

proof end;

Lemma13: for b₁ being Nat
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂ st 1 <= b₁ & b₁ <= len b₃ holds
( the Source of b₂ . (b₃ . b₁) in the Vertices of b₂ & the Target of b₂ . (b₃ . b₁) in the Vertices of b₂ )

proof end;

theorem Th11: :: GRAPHSP:11

for b₁ being Graph
for b₂, b₃ being set
for b₄, b₅ being Vertex of b₁ st the Vertices of b₁ = b₂ \/ b₃ & b₄ in b₂ & b₅ in b₃ & ( for b₆, b₇ being Vertex of b₁ st b₆ in b₂ & b₇ in b₃ holds
for b₈ being set holds
( not b₈ in the Edges of b₁ or not b₈ orientedly_joins b₆,b₇ ) ) holds
for b₆ being oriented Chain of b₁ holds not b₆ is_orientedpath_of b₄,b₅

proof end;

Lemma15: for b₁ being Nat
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂
for b₄ being Vertex of b₂ st 1 <= b₁ & b₁ <= len b₃ & ( b₄ = the Source of b₂ . (b₃ . b₁) or b₄ = the Target of b₂ . (b₃ . b₁) ) holds
b₄ in vertices b₃

proof end;

theorem Th12: :: GRAPHSP:12

for b₁ being Graph
for b₂ being oriented Chain of b₁
for b₃, b₄ being set
for b₅, b₆ being Vertex of b₁ st the Vertices of b₁ = b₃ \/ b₄ & b₅ in b₃ & ( for b₇, b₈ being Vertex of b₁ st b₇ in b₃ & b₈ in b₄ holds
for b₉ being set holds
( not b₉ in the Edges of b₁ or not b₉ orientedly_joins b₇,b₈ ) ) & b₂ is_orientedpath_of b₅,b₆ holds
b₂ is_orientedpath_of b₅,b₆,b₃

proof end;

theorem Th13: :: GRAPHSP:13

for b₁ being Function
for b₂ being set
for b₃ being finite Graph
for b₄, b₅ being oriented Chain of b₃
for b₆, b₇, b₈ being Vertex of b₃ st b₁ is_weight>=0of b₃ & b₄ is_shortestpath_of b₆,b₇,b₂,b₁ & b₆ <> b₇ & b₆ <> b₈ & b₅ is_shortestpath_of b₆,b₈,b₂,b₁ & ( for b₉ being set holds
( not b₉ in the Edges of b₃ or not b₉ orientedly_joins b₇,b₈ ) ) & b₄ islongestInShortestpath b₂,b₆,b₁ holds
b₅ is_shortestpath_of b₆,b₈,b₂ \/ {b₇},b₁

proof end;

theorem Th14: :: GRAPHSP:14

for b₁ being set
for b₂ being oriented finite Graph
for b₃ being oriented Chain of b₂
for b₄ being Function of the Edges of b₂, Real>=0
for b₅, b₆ being Vertex of b₂ st b₁ in the Edges of b₂ & b₅ <> b₆ & b₃ = <*b₁*> & b₁ orientedly_joins b₅,b₆ holds
b₃ is_shortestpath_of b₅,b₆,{b₅},b₄

proof end;

theorem Th15: :: GRAPHSP:15

for b₁, b₂ being set
for b₃ being oriented finite Graph
for b₄, b₅ being oriented Chain of b₃
for b₆ being Function of the Edges of b₃, Real>=0
for b₇, b₈, b₉ being Vertex of b₃ st b₁ in the Edges of b₃ & b₄ is_shortestpath_of b₇,b₈,b₂,b₆ & b₇ <> b₉ & b₅ = b₄ ^ <*b₁*> & b₁ orientedly_joins b₈,b₉ & b₇ in b₂ & ( for b₁₀ being Vertex of b₃ st b₁₀ in b₂ holds
for b₁₁ being set holds
( not b₁₁ in the Edges of b₃ or not b₁₁ orientedly_joins b₁₀,b₉ ) ) holds
b₅ is_shortestpath_of b₇,b₉,b₂ \/ {b₈},b₆

proof end;

theorem Th16: :: GRAPHSP:16

for b₁, b₂ being set
for b₃ being oriented finite Graph
for b₄ being oriented Chain of b₃
for b₅ being Function of the Edges of b₃, Real>=0
for b₆, b₇ being Vertex of b₃ st the Vertices of b₃ = b₁ \/ b₂ & b₆ in b₁ & ( for b₈, b₉ being Vertex of b₃ st b₈ in b₁ & b₉ in b₂ holds
for b₁₀ being set holds
( not b₁₀ in the Edges of b₃ or not b₁₀ orientedly_joins b₈,b₉ ) ) holds
( b₄ is_shortestpath_of b₆,b₇,b₁,b₅ iff b₄ is_shortestpath_of b₆,b₇,b₅ )

proof end;

notation

let c₁ be Function;
let c₂, c₃ be set ;
synonym c₁,c₂ := c₃ for c₁ +* c₂,c₃;

end;

theorem Th17: :: GRAPHSP:17

for b₁, b₂ being set
for b₃ being Function holds rng (b₃,b₁ := b₂) c= (rng b₃) \/ {b₂}

proof end;

definition

let c₁ be FinSequence of REAL ;
let c₂ be set ;
let c₃ be Real;
redefine func := as c₁,c₂ := c₃ -> FinSequence of REAL ;
coherence

proof end;

end;

definition

let c₁, c₂ be Nat;
let c₃ be FinSequence of REAL ;
let c₄ be Real;
func c₃,c₁ := c₂,c₄ -> FinSequence of REAL equals :: GRAPHSP:def 1
(a₃,a₁ := a₂),a₂ := a₄;
coherence ;

end;

:: deftheorem Def1 defines := GRAPHSP:def 1 :

theorem Th18: :: GRAPHSP:18

for b₁, b₂ being Nat
for b₃ being Element of REAL *
for b₄ being Real st b₁ <> b₂ & b₁ in dom b₃ holds
(b₃,b₁ := b₂,b₄) . b₁ = b₂

proof end;

theorem Th19: :: GRAPHSP:19

for b₁, b₂, b₃ being Nat
for b₄ being Element of REAL *
for b₅ being Real st b₁ <> b₂ & b₁ <> b₃ & b₁ in dom b₄ holds
(b₄,b₂ := b₃,b₅) . b₁ = b₄ . b₁

proof end;

theorem Th20: :: GRAPHSP:20

for b₁, b₂ being Nat
for b₃ being Element of REAL *
for b₄ being Real st b₁ in dom b₃ holds
(b₃,b₂ := b₁,b₄) . b₁ = b₄

proof end;

theorem Th21: :: GRAPHSP:21

for b₁, b₂ being Nat
for b₃ being Element of REAL *
for b₄ being Real holds dom (b₃,b₁ := b₂,b₄) = dom b₃

proof end;

definition

let c₁ be set ;
redefine func id as id c₁ -> Element of Funcs a₁,a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be Function of c₁,c₁;
redefine func * as c₃ * c₂ -> Function of a₁,a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂, c₃ be Element of Funcs c₁,c₁;
redefine func * as c₃ * c₂ -> Element of Funcs a₁,a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Element of Funcs c₁,c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> Element of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Element of Funcs c₁,c₁;
func repeat c₂ -> Function of NAT , Funcs a₁,a₁ means :Def2: :: GRAPHSP:def 2
( a₃ . 0 = id a₁ & ( for b₁ being Nat holds a₃ . (b₁ + 1) = a₂ * (a₃ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines repeat GRAPHSP:def 2 :

theorem Th22: :: GRAPHSP:22

for b₁ being Element of Funcs (REAL * ),(REAL * )
for b₂ being Element of REAL *
for b₃, b₄ being Nat holds ((repeat b₁) . 0) . b₂ = b₂

proof end;

Lemma28: for b₁ being set
for b₂ being Element of Funcs b₁,b₁ holds dom b₂ = b₁

proof end;

theorem Th23: :: GRAPHSP:23

for b₁, b₂ being Element of Funcs (REAL * ),(REAL * )
for b₃ being Element of REAL *
for b₄ being Nat holds ((repeat (b₁ * b₂)) . (b₄ + 1)) . b₃ = b₁ . (b₂ . (((repeat (b₁ * b₂)) . b₄) . b₃))

proof end;

definition

let c₁ be Element of Funcs (REAL * ),(REAL * );
let c₂ be Element of REAL * ;
redefine func . as c₁ . c₂ -> Element of REAL * ;
coherence

proof end;

end;

definition

let c₁ be Element of REAL * ;
let c₂ be Nat;
func OuterVx c₁,c₂ -> Subset of NAT equals :: GRAPHSP:def 3
{ b₁ where B is Nat : ( b₁ in dom a₁ & 1 <= b₁ & b₁ <= a₂ & a₁ . b₁ <> - 1 & a₁ . (a₂ + b₁) <> - 1 ) } ;
coherence

proof end;

end;

:: deftheorem Def3 defines OuterVx GRAPHSP:def 3 :

definition

let c₁ be Element of Funcs (REAL * ),(REAL * );
let c₂ be Element of REAL * ;
let c₃ be Nat;
assume E30: ex b₁ being Nat st OuterVx (((repeat c₁) . b₁) . c₂),c₃ = {} ;
func LifeSpan c₁,c₂,c₃ -> Nat means :Def4: :: GRAPHSP:def 4
( OuterVx (((repeat a₁) . a₄) . a₂),a₃ = {} & ( for b₁ being Nat st OuterVx (((repeat a₁) . b₁) . a₂),a₃ = {} holds
a₄ <= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines LifeSpan GRAPHSP:def 4 :

definition

let c₁ be Element of Funcs (REAL * ),(REAL * );
let c₂ be Nat;
func while_do c₁,c₂ -> Element of Funcs (REAL * ),(REAL * ) means :Def5: :: GRAPHSP:def 5
( dom a₃ = REAL * & ( for b₁ being Element of REAL * holds a₃ . b₁ = ((repeat a₁) . (LifeSpan a₁,b₁,a₂)) . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines while_do GRAPHSP:def 5 :

definition

let c₁ be oriented Graph;
let c₂, c₃ be Vertex of c₁;
assume E32: ex b₁ being set st
( b₁ in the Edges of c₁ & b₁ orientedly_joins c₂,c₃ ) ;
func Edge c₂,c₃ -> set means :Def6: :: GRAPHSP:def 6
ex b₁ being set st
( a₄ = b₁ & b₁ in the Edges of a₁ & b₁ orientedly_joins a₂,a₃ );
existence by E32;
uniqueness by Th10;

end;

:: deftheorem Def6 defines Edge GRAPHSP:def 6 :

definition

let c₁ be oriented Graph;
let c₂, c₃ be Vertex of c₁;
let c₄ be Function;
func Weight c₂,c₃,c₄ -> set equals :Def7: :: GRAPHSP:def 7
a₄ . (Edge a₂,a₃) if ex b₁ being set st
( b₁ in the Edges of a₁ & b₁ orientedly_joins a₂,a₃ )
otherwise - 1;
correctness ;

end;

:: deftheorem Def7 defines Weight GRAPHSP:def 7 :

definition

let c₁ be oriented Graph;
let c₂, c₃ be Vertex of c₁;
let c₄ be Function of the Edges of c₁, Real>=0 ;
redefine func Weight as Weight c₂,c₃,c₄ -> Real;
coherence

proof end;

end;

theorem Th24: :: GRAPHSP:24

for b₁ being oriented Graph
for b₂, b₃ being Vertex of b₁
for b₄ being Function of the Edges of b₁, Real>=0 holds
( Weight b₂,b₃,b₄ >= 0 iff ex b₅ being set st
( b₅ in the Edges of b₁ & b₅ orientedly_joins b₂,b₃ ) )

proof end;

theorem Th25: :: GRAPHSP:25

for b₁ being oriented Graph
for b₂, b₃ being Vertex of b₁
for b₄ being Function of the Edges of b₁, Real>=0 holds
( Weight b₂,b₃,b₄ = - 1 iff for b₅ being set holds
( not b₅ in the Edges of b₁ or not b₅ orientedly_joins b₂,b₃ ) ) by Def7, Th24;

theorem Th26: :: GRAPHSP:26

for b₁ being set
for b₂ being oriented Graph
for b₃, b₄ being Vertex of b₂
for b₅ being Function of the Edges of b₂, Real>=0 st b₁ in the Edges of b₂ & b₁ orientedly_joins b₃,b₄ holds
Weight b₃,b₄,b₅ = b₅ . b₁

proof end;

definition

let c₁ be Element of REAL * ;
let c₂ be Nat;
func UnusedVx c₁,c₂ -> Subset of NAT equals :: GRAPHSP:def 8
{ b₁ where B is Nat : ( b₁ in dom a₁ & 1 <= b₁ & b₁ <= a₂ & a₁ . b₁ <> - 1 ) } ;
coherence

proof end;

end;

:: deftheorem Def8 defines UnusedVx GRAPHSP:def 8 :

definition

let c₁ be Element of REAL * ;
let c₂ be Nat;
func UsedVx c₁,c₂ -> Subset of NAT equals :: GRAPHSP:def 9
{ b₁ where B is Nat : ( b₁ in dom a₁ & 1 <= b₁ & b₁ <= a₂ & a₁ . b₁ = - 1 ) } ;
coherence

proof end;

end;

:: deftheorem Def9 defines UsedVx GRAPHSP:def 9 :

theorem Th27: :: GRAPHSP:27

for b₁ being Nat
for b₂ being Element of REAL * holds UnusedVx b₂,b₁ c= Seg b₁

proof end;

registration

let c₁ be Element of REAL * ;
let c₂ be Nat;
cluster UnusedVx a₁,a₂ -> finite ;
coherence

proof end;

end;

theorem Th28: :: GRAPHSP:28

for b₁ being Nat
for b₂ being Element of REAL * holds OuterVx b₂,b₁ c= UnusedVx b₂,b₁

proof end;

theorem Th29: :: GRAPHSP:29

for b₁ being Nat
for b₂ being Element of REAL * holds OuterVx b₂,b₁ c= Seg b₁

proof end;

registration

let c₁ be Element of REAL * ;
let c₂ be Nat;
cluster OuterVx a₁,a₂ -> finite ;
coherence

proof end;

end;

definition

let c₁ be finite Subset of NAT ;
let c₂ be Element of REAL * ;
let c₃ be Nat;
func Argmin c₁,c₂,c₃ -> Nat means :Def10: :: GRAPHSP:def 10
( ( a₁ <> {} implies ex b₁ being Nat st
( b₁ = a₄ & b₁ in a₁ & ( for b₂ being Nat st b₂ in a₁ holds
a₂ /. ((2 * a₃) + b₁) <= a₂ /. ((2 * a₃) + b₂) ) & ( for b₂ being Nat st b₂ in a₁ & a₂ /. ((2 * a₃) + b₁) = a₂ /. ((2 * a₃) + b₂) holds
b₁ <= b₂ ) ) ) & ( a₁ = {} implies a₄ = 0 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines Argmin GRAPHSP:def 10 :

theorem Th30: :: GRAPHSP:30

for b₁, b₂ being Nat
for b₃ being Element of REAL * st OuterVx b₃,b₁ <> {} & b₂ = Argmin (OuterVx b₃,b₁),b₃,b₁ holds
( b₂ in dom b₃ & 1 <= b₂ & b₂ <= b₁ & b₃ . b₂ <> - 1 & b₃ . (b₁ + b₂) <> - 1 )

proof end;

theorem Th31: :: GRAPHSP:31

for b₁ being Nat
for b₂ being Element of REAL * holds Argmin (OuterVx b₂,b₁),b₂,b₁ <= b₁

proof end;

definition

let c₁ be Nat;
func findmin c₁ -> Element of Funcs (REAL * ),(REAL * ) means :Def11: :: GRAPHSP:def 11
( dom a₂ = REAL * & ( for b₁ being Element of REAL * holds a₂ . b₁ = b₁,(((a₁ * a₁) + (3 * a₁)) + 1) := (Argmin (OuterVx b₁,a₁),b₁,a₁),(- 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines findmin GRAPHSP:def 11 :

theorem Th32: :: GRAPHSP:32

for b₁, b₂ being Nat
for b₃ being Element of REAL * st b₁ in dom b₃ & b₁ > b₂ & b₁ <> ((b₂ * b₂) + (3 * b₂)) + 1 holds
((findmin b₂) . b₃) . b₁ = b₃ . b₁

proof end;

theorem Th33: :: GRAPHSP:33

for b₁, b₂ being Nat
for b₃ being Element of REAL * st b₁ in dom b₃ & b₃ . b₁ = - 1 & b₁ <> ((b₂ * b₂) + (3 * b₂)) + 1 holds
((findmin b₂) . b₃) . b₁ = - 1

proof end;

theorem Th34: :: GRAPHSP:34

for b₁ being Nat
for b₂ being Element of REAL * holds dom ((findmin b₁) . b₂) = dom b₂

proof end;

Lemma46: for b₁, b₂ being Nat st b₁ >= 1 holds
b₂ <= b₁ * b₂

proof end;

Lemma47: for b₁ being Nat holds
( 3 * b₁ < ((b₁ * b₁) + (3 * b₁)) + 1 & b₁ < ((b₁ * b₁) + (3 * b₁)) + 1 & 2 * b₁ < ((b₁ * b₁) + (3 * b₁)) + 1 )

proof end;

Lemma48: for b₁, b₂ being Nat holds
( ( b₁ < b₂ & b₂ <= 2 * b₁ implies ( ( not 2 * b₁ < b₂ or not b₂ <= 3 * b₁ ) & not b₂ <= b₁ & not b₂ > 3 * b₁ ) ) & ( ( b₂ <= b₁ or b₂ > 3 * b₁ ) implies ( ( not 2 * b₁ < b₂ or not b₂ <= 3 * b₁ ) & ( not b₁ < b₂ or not b₂ <= 2 * b₁ ) ) ) & ( 2 * b₁ < b₂ & b₂ <= 3 * b₁ implies ( ( not b₁ < b₂ or not b₂ <= 2 * b₁ ) & not b₂ <= b₁ & not b₂ > 3 * b₁ ) ) )

proof end;

theorem Th35: :: GRAPHSP:35

for b₁ being Nat
for b₂ being Element of REAL * st OuterVx b₂,b₁ <> {} holds
ex b₃ being Nat st
( b₃ in OuterVx b₂,b₁ & 1 <= b₃ & b₃ <= b₁ & ((findmin b₁) . b₂) . b₃ = - 1 )

proof end;

definition

let c₁ be Element of REAL * ;
let c₂, c₃ be Nat;
func newpathcost c₁,c₂,c₃ -> Real equals :: GRAPHSP:def 12
(a₁ /. ((2 * a₂) + (a₁ /. (((a₂ * a₂) + (3 * a₂)) + 1)))) + (a₁ /. (((2 * a₂) + (a₂ * (a₁ /. (((a₂ * a₂) + (3 * a₂)) + 1)))) + a₃));
correctness ;

end;

:: deftheorem Def12 defines newpathcost GRAPHSP:def 12 :

definition

let c₁, c₂ be Nat;
let c₃ be Element of REAL * ;
pred c₃ hasBetterPathAt c₁,c₂ means :Def13: :: GRAPHSP:def 13
( ( a₃ . (a₁ + a₂) = - 1 or a₃ /. ((2 * a₁) + a₂) > newpathcost a₃,a₁,a₂ ) & a₃ /. (((2 * a₁) + (a₁ * (a₃ /. (((a₁ * a₁) + (3 * a₁)) + 1)))) + a₂) >= 0 & a₃ . a₂ <> - 1 );

end;

:: deftheorem Def13 defines hasBetterPathAt GRAPHSP:def 13 :

definition

let c₁ be Element of REAL * ;
let c₂ be Nat;
func Relax c₁,c₂ -> Element of REAL * means :Def14: :: GRAPHSP:def 14
( dom a₃ = dom a₁ & ( for b₁ being Nat st b₁ in dom a₁ holds
( ( a₂ < b₁ & b₁ <= 2 * a₂ implies ( ( a₁ hasBetterPathAt a₂,b₁ -' a₂ implies a₃ . b₁ = a₁ /. (((a₂ * a₂) + (3 * a₂)) + 1) ) & ( not a₁ hasBetterPathAt a₂,b₁ -' a₂ implies a₃ . b₁ = a₁ . b₁ ) ) ) & ( 2 * a₂ < b₁ & b₁ <= 3 * a₂ implies ( ( a₁ hasBetterPathAt a₂,b₁ -' (2 * a₂) implies a₃ . b₁ = newpathcost a₁,a₂,(b₁ -' (2 * a₂)) ) & ( not a₁ hasBetterPathAt a₂,b₁ -' (2 * a₂) implies a₃ . b₁ = a₁ . b₁ ) ) ) & ( ( b₁ <= a₂ or b₁ > 3 * a₂ ) implies a₃ . b₁ = a₁ . b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines Relax GRAPHSP:def 14 :

definition

let c₁ be Nat;
func Relax c₁ -> Element of Funcs (REAL * ),(REAL * ) means :Def15: :: GRAPHSP:def 15
( dom a₂ = REAL * & ( for b₁ being Element of REAL * holds a₂ . b₁ = Relax b₁,a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Relax GRAPHSP:def 15 :

theorem Th36: :: GRAPHSP:36

for b₁ being Nat
for b₂ being Element of REAL * holds dom ((Relax b₁) . b₂) = dom b₂

proof end;

theorem Th37: :: GRAPHSP:37

for b₁, b₂ being Nat
for b₃ being Element of REAL * st ( b₁ <= b₂ or b₁ > 3 * b₂ ) & b₁ in dom b₃ holds
((Relax b₂) . b₃) . b₁ = b₃ . b₁

proof end;

theorem Th38: :: GRAPHSP:38

for b₁, b₂ being Nat
for b₃ being Element of REAL * holds dom (((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₃) = dom (((repeat ((Relax b₁) * (findmin b₁))) . (b₂ + 1)) . b₃)

proof end;

theorem Th39: :: GRAPHSP:39

for b₁, b₂ being Nat
for b₃ being Element of REAL * st OuterVx (((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₃),b₁ <> {} holds
UnusedVx (((repeat ((Relax b₁) * (findmin b₁))) . (b₂ + 1)) . b₃),b₁ c< UnusedVx (((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₃),b₁

proof end;

theorem Th40: :: GRAPHSP:40

for b₁, b₂, b₃ being Nat
for b₄, b₅, b₆ being Element of REAL * st b₄ = ((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₅ & b₆ = ((repeat ((Relax b₁) * (findmin b₁))) . (b₂ + 1)) . b₅ & b₃ = Argmin (OuterVx b₄,b₁),b₄,b₁ & OuterVx b₄,b₁ <> {} holds
( UsedVx b₆,b₁ = (UsedVx b₄,b₁) \/ {b₃} & not b₃ in UsedVx b₄,b₁ )

proof end;

theorem Th41: :: GRAPHSP:41

for b₁ being Nat
for b₂ being Element of REAL * ex b₃ being Nat st
( b₃ <= b₁ & OuterVx (((repeat ((Relax b₁) * (findmin b₁))) . b₃) . b₂),b₁ = {} )

proof end;

Lemma59: for b₁, b₂ being Nat holds b₁ - b₂ <= b₁

proof end;

Lemma60: for b₁, b₂ being FinSequence of NAT
for b₃ being Element of REAL *
for b₄, b₅ being Nat st ( for b₆ being Nat st 1 <= b₆ & b₆ < len b₁ holds
b₁ . ((len b₁) - b₆) = b₃ . ((b₁ /. (((len b₁) - b₆) + 1)) + b₅) ) & ( for b₆ being Nat st 1 <= b₆ & b₆ < len b₂ holds
b₂ . ((len b₂) - b₆) = b₃ . ((b₂ /. (((len b₂) - b₆) + 1)) + b₅) ) & len b₁ <= len b₂ & b₁ . (len b₁) = b₂ . (len b₂) holds
for b₆ being Nat st 1 <= b₆ & b₆ < len b₁ holds
b₁ . ((len b₁) - b₆) = b₂ . ((len b₂) - b₆)

proof end;

theorem Th42: :: GRAPHSP:42

for b₁, b₂ being Nat
for b₃ being Element of REAL * holds dom b₃ = dom (((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₃)

proof end;

definition

let c₁, c₂ be Element of REAL * ;
let c₃, c₄ be Nat;
pred c₁,c₂ equal_at c₃,c₄ means :Def16: :: GRAPHSP:def 16
( dom a₁ = dom a₂ & ( for b₁ being Nat st b₁ in dom a₁ & a₃ <= b₁ & b₁ <= a₄ holds
a₁ . b₁ = a₂ . b₁ ) );

end;

:: deftheorem Def16 defines equal_at GRAPHSP:def 16 :

theorem Th43: :: GRAPHSP:43

for b₁, b₂ being Nat
for b₃ being Element of REAL * holds b₃,b₃ equal_at b₁,b₂

proof end;

theorem Th44: :: GRAPHSP:44

for b₁, b₂ being Nat
for b₃, b₄, b₅ being Element of REAL * st b₃,b₄ equal_at b₁,b₂ & b₄,b₅ equal_at b₁,b₂ holds
b₃,b₅ equal_at b₁,b₂

proof end;

theorem Th45: :: GRAPHSP:45

for b₁, b₂ being Nat
for b₃ being Element of REAL * holds ((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₃,((repeat ((Relax b₁) * (findmin b₁))) . (b₂ + 1)) . b₃ equal_at (3 * b₁) + 1,(b₁ * b₁) + (3 * b₁)

proof end;

theorem Th46: :: GRAPHSP:46

for b₁ being Element of Funcs (REAL * ),(REAL * )
for b₂ being Element of REAL *
for b₃, b₄ being Nat st b₄ < LifeSpan b₁,b₂,b₃ holds
OuterVx (((repeat b₁) . b₄) . b₂),b₃ <> {} by Def4;

theorem Th47: :: GRAPHSP:47

for b₁, b₂ being Nat
for b₃ being Element of REAL * holds b₃,((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₃ equal_at (3 * b₁) + 1,(b₁ * b₁) + (3 * b₁)

proof end;

theorem Th48: :: GRAPHSP:48

for b₁ being Nat
for b₂ being Element of REAL * st 1 <= b₁ & 1 in dom b₂ & b₂ . (b₁ + 1) <> - 1 & ( for b₃ being Nat st 1 <= b₃ & b₃ <= b₁ holds
b₂ . b₃ = 1 ) & ( for b₃ being Nat st 2 <= b₃ & b₃ <= b₁ holds
b₂ . (b₁ + b₃) = - 1 ) holds
( 1 = Argmin (OuterVx b₂,b₁),b₂,b₁ & UsedVx b₂,b₁ = {} & {1} = UsedVx (((repeat ((Relax b₁) * (findmin b₁))) . 1) . b₂),b₁ )

proof end;

theorem Th49: :: GRAPHSP:49

for b₁, b₂, b₃ being Nat
for b₄, b₅, b₆ being Element of REAL * st b₄ = ((repeat ((Relax b₁) * (findmin b₁))) . 1) . b₅ & b₆ = ((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₅ & 1 <= b₂ & b₂ <= LifeSpan ((Relax b₁) * (findmin b₁)),b₅,b₁ & b₃ in UsedVx b₄,b₁ holds
b₃ in UsedVx b₆,b₁

proof end;

definition

let c₁ be FinSequence of NAT ;
let c₂ be Element of REAL * ;
let c₃, c₄ be Nat;
pred c₁ is_vertex_seq_at c₂,c₃,c₄ means :Def17: :: GRAPHSP:def 17
( a₁ . (len a₁) = a₃ & ( for b₁ being Nat st 1 <= b₁ & b₁ < len a₁ holds
a₁ . ((len a₁) - b₁) = a₂ . (a₄ + (a₁ /. (((len a₁) - b₁) + 1))) ) );

end;

:: deftheorem Def17 defines is_vertex_seq_at GRAPHSP:def 17 :

definition

let c₁ be FinSequence of NAT ;
let c₂ be Element of REAL * ;
let c₃, c₄ be Nat;
pred c₁ is_simple_vertex_seq_at c₂,c₃,c₄ means :Def18: :: GRAPHSP:def 18
( a₁ . 1 = 1 & len a₁ > 1 & a₁ is_vertex_seq_at a₂,a₃,a₄ & a₁ is one-to-one );

end;

:: deftheorem Def18 defines is_simple_vertex_seq_at GRAPHSP:def 18 :

theorem Th50: :: GRAPHSP:50

for b₁, b₂ being FinSequence of NAT
for b₃ being Element of REAL *
for b₄, b₅ being Nat st b₁ is_simple_vertex_seq_at b₃,b₄,b₅ & b₂ is_simple_vertex_seq_at b₃,b₄,b₅ holds
b₁ = b₂

proof end;

definition

let c₁ be Graph;
let c₂ be FinSequence of the Edges of c₁;
let c₃ be FinSequence;
pred c₂ is_oriented_edge_seq_of c₃ means :Def19: :: GRAPHSP:def 19
( len a₃ = (len a₂) + 1 & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₂ holds
( the Source of a₁ . (a₂ . b₁) = a₃ . b₁ & the Target of a₁ . (a₂ . b₁) = a₃ . (b₁ + 1) ) ) );

end;

:: deftheorem Def19 defines is_oriented_edge_seq_of GRAPHSP:def 19 :

theorem Th51: :: GRAPHSP:51

for b₁ being oriented Graph
for b₂ being FinSequence
for b₃, b₄ being oriented Chain of b₁ st b₃ is_oriented_edge_seq_of b₂ & b₄ is_oriented_edge_seq_of b₂ holds
b₃ = b₄

proof end;

theorem Th52: :: GRAPHSP:52

for b₁ being Graph
for b₂, b₃ being FinSequence
for b₄ being oriented Chain of b₁ st b₄ is_oriented_edge_seq_of b₂ & b₄ is_oriented_edge_seq_of b₃ & len b₄ >= 1 holds
b₂ = b₃

proof end;

Lemma72: for b₁, b₂ being Nat st 1 <= b₁ & b₁ <= b₂ holds
( 1 < (2 * b₂) + b₁ & (2 * b₂) + b₁ < ((b₂ * b₂) + (3 * b₂)) + 1 & b₁ < (2 * b₂) + b₁ )

proof end;

Lemma73: for b₁, b₂ being Nat st 1 <= b₁ & b₁ <= b₂ holds
( 1 < b₂ + b₁ & b₂ + b₁ <= 2 * b₂ & b₂ + b₁ < ((b₂ * b₂) + (3 * b₂)) + 1 )

proof end;

Lemma74: for b₁, b₂, b₃ being Nat st 1 <= b₁ & b₁ <= b₂ & b₃ <= b₂ holds
( 1 < ((2 * b₂) + (b₂ * b₁)) + b₃ & b₁ < ((2 * b₂) + (b₂ * b₁)) + b₃ & ((2 * b₂) + (b₂ * b₁)) + b₃ < ((b₂ * b₂) + (3 * b₂)) + 1 )

proof end;

Lemma75: for b₁, b₂, b₃ being Nat st 1 <= b₁ & b₁ <= b₂ & 1 <= b₃ & b₃ <= b₂ holds
( (3 * b₂) + 1 <= ((2 * b₂) + (b₂ * b₁)) + b₃ & ((2 * b₂) + (b₂ * b₁)) + b₃ <= (b₂ * b₂) + (3 * b₂) )

proof end;

definition

let c₁ be Element of REAL * ;
let c₂ be oriented Graph;
let c₃ be Nat;
let c₄ be Function of the Edges of c₂, Real>=0 ;
pred c₁ is_Input_of_Dijkstra_Alg c₂,c₃,c₄ means :Def20: :: GRAPHSP:def 20
( len a₁ = ((a₃ * a₃) + (3 * a₃)) + 1 & Seg a₃ = the Vertices of a₂ & ( for b₁ being Nat st 1 <= b₁ & b₁ <= a₃ holds
( a₁ . b₁ = 1 & a₁ . ((2 * a₃) + b₁) = 0 ) ) & a₁ . (a₃ + 1) = 0 & ( for b₁ being Nat st 2 <= b₁ & b₁ <= a₃ holds
a₁ . (a₃ + b₁) = - 1 ) & ( for b₁, b₂ being Vertex of a₂
for b₃, b₄ being Nat st b₃ = b₁ & b₄ = b₂ holds
a₁ . (((2 * a₃) + (a₃ * b₃)) + b₄) = Weight b₁,b₂,a₄ ) );

end;

:: deftheorem Def20 defines is_Input_of_Dijkstra_Alg GRAPHSP:def 20 :

definition

let c₁ be Nat;
func DijkstraAlgorithm c₁ -> Element of Funcs (REAL * ),(REAL * ) equals :: GRAPHSP:def 21
while_do ((Relax a₁) * (findmin a₁)),a₁;
coherence ;

end;

:: deftheorem Def21 defines DijkstraAlgorithm GRAPHSP:def 21 :

Lemma77: for b₁ being Nat
for b₂, b₃ being Element of REAL *
for b₄ being oriented finite Graph
for b₅ being Function of the Edges of b₄, Real>=0
for b₆ being Vertex of b₄ st b₂ is_Input_of_Dijkstra_Alg b₄,b₁,b₅ & b₆ = 1 & b₁ >= 1 & b₃ = ((repeat ((Relax b₁) * (findmin b₁))) . 1) . b₂ holds
( ( for b₇ being Vertex of b₄
for b₈ being Nat st b₇ <> b₆ & b₇ = b₈ & b₃ . (b₁ + b₈) <> - 1 holds
ex b₉ being FinSequence of NAT ex b₁₀ being oriented Chain of b₄ st
( b₉ is_simple_vertex_seq_at b₃,b₈,b₁ & ( for b₁₁ being Nat st 1 <= b₁₁ & b₁₁ < len b₉ holds
b₉ . b₁₁ in UsedVx b₃,b₁ ) & b₁₀ is_oriented_edge_seq_of b₉ & b₁₀ is_shortestpath_of b₆,b₇, UsedVx b₃,b₁,b₅ & cost b₁₀,b₅ = b₃ . ((2 * b₁) + b₈) & ( not b₇ in UsedVx b₃,b₁ implies b₁₀ islongestInShortestpath UsedVx b₃,b₁,b₆,b₅ ) ) ) & ( for b₇, b₈ being Nat st b₃ . (b₁ + b₈) = - 1 & 1 <= b₈ & b₈ <= b₁ & b₇ in UsedVx b₃,b₁ holds
b₂ . (((2 * b₁) + (b₁ * b₇)) + b₈) = - 1 ) & ( for b₇ being Nat st b₇ in UsedVx b₃,b₁ holds
b₃ . (b₁ + b₇) <> - 1 ) )

proof end;

Lemma78: for b₁, b₂, b₃ being Nat
for b₄, b₅, b₆ being Element of REAL * st b₄ = ((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₅ & b₆ = ((repeat ((Relax b₁) * (findmin b₁))) . (b₂ + 1)) . b₅ & OuterVx b₄,b₁ <> {} & b₃ in UsedVx b₄,b₁ & len b₅ = ((b₁ * b₁) + (3 * b₁)) + 1 holds
b₆ . (b₁ + b₃) = b₄ . (b₁ + b₃)

proof end;

Lemma79: for b₁, b₂, b₃ being Nat
for b₄, b₅, b₆ being Element of REAL *
for b₇ being FinSequence of NAT st b₄ = ((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₅ & b₆ = ((repeat ((Relax b₁) * (findmin b₁))) . (b₂ + 1)) . b₅ & OuterVx b₄,b₁ <> {} & len b₅ = ((b₁ * b₁) + (3 * b₁)) + 1 & b₇ is_simple_vertex_seq_at b₄,b₃,b₁ & b₄ . (b₁ + b₃) = b₆ . (b₁ + b₃) & ( for b₈ being Nat st 1 <= b₈ & b₈ < len b₇ holds
b₇ . b₈ in UsedVx b₄,b₁ ) holds
b₇ is_simple_vertex_seq_at b₆,b₃,b₁

proof end;

Lemma80: for b₁, b₂, b₃, b₄ being Nat
for b₅, b₆, b₇ being Element of REAL *
for b₈ being FinSequence of NAT st b₅ = ((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₆ & b₇ = ((repeat ((Relax b₁) * (findmin b₁))) . (b₂ + 1)) . b₆ & OuterVx b₅,b₁ <> {} & len b₆ = ((b₁ * b₁) + (3 * b₁)) + 1 & b₈ is_simple_vertex_seq_at b₅,b₃,b₁ & b₃ = b₇ . (b₁ + b₄) & b₅ . (b₁ + b₃) = b₇ . (b₁ + b₃) & b₃ <> b₄ & not b₄ in UsedVx b₅,b₁ & ( for b₉ being Nat st 1 <= b₉ & b₉ < len b₈ holds
b₈ . b₉ in UsedVx b₅,b₁ ) holds
b₈ ^ <*b₄*> is_simple_vertex_seq_at b₇,b₄,b₁

proof end;

Lemma81: for b₁, b₂ being Nat
for b₃ being set
for b₄, b₅ being Element of REAL *
for b₆ being oriented finite Graph
for b₇ being oriented Chain of b₆
for b₈ being Function of the Edges of b₆, Real>=0
for b₉, b₁₀ being Vertex of b₆ st b₄ is_Input_of_Dijkstra_Alg b₆,b₁,b₈ & b₈ is_weight>=0of b₆ & b₉ = b₂ & b₁₀ <> b₉ & 1 <= b₂ & b₂ <= b₁ & b₇ is_shortestpath_of b₁₀,b₉,b₃,b₈ & ( for b₁₁, b₁₂ being Nat st b₅ . (b₁ + b₁₂) = - 1 & 1 <= b₁₂ & b₁₂ <= b₁ & b₁₁ in b₃ holds
b₄ . (((2 * b₁) + (b₁ * b₁₁)) + b₁₂) = - 1 ) holds
b₅ . (b₁ + b₂) <> - 1

proof end;

Lemma82: for b₁, b₂ being Nat
for b₃, b₄, b₅ being Element of REAL *
for b₆ being oriented finite Graph
for b₇ being Function of the Edges of b₆, Real>=0
for b₈ being Vertex of b₆ st b₃ is_Input_of_Dijkstra_Alg b₆,b₁,b₇ & b₈ = 1 & b₁ >= 1 & b₄ = ((repeat ((Relax b₁) * (findmin b₁))) . b₂) . b₃ & b₅ = ((repeat ((Relax b₁) * (findmin b₁))) . (b₂ + 1)) . b₃ & OuterVx b₄,b₁ <> {} & b₂ >= 1 & 1 in UsedVx b₄,b₁ & ( for b₉ being Vertex of b₆
for b₁₀ being Nat st b₉ <> b₈ & b₉ = b₁₀ & b₄ . (b₁ + b₁₀) <> - 1 holds
ex b₁₁ being FinSequence of NAT ex b₁₂ being oriented Chain of b₆ st
( b₁₁ is_simple_vertex_seq_at b₄,b₁₀,b₁ & ( for b₁₃ being Nat st 1 <= b₁₃ & b₁₃ < len b₁₁ holds
b₁₁ . b₁₃ in UsedVx b₄,b₁ ) & b₁₂ is_oriented_edge_seq_of b₁₁ & b₁₂ is_shortestpath_of b₈,b₉, UsedVx b₄,b₁,b₇ & cost b₁₂,b₇ = b₄ . ((2 * b₁) + b₁₀) & ( not b₉ in UsedVx b₄,b₁ implies b₁₂ islongestInShortestpath UsedVx b₄,b₁,b₈,b₇ ) ) ) & ( for b₉, b₁₀ being Nat st b₄ . (b₁ + b₁₀) = - 1 & 1 <= b₁₀ & b₁₀ <= b₁ & b₉ in UsedVx b₄,b₁ holds
b₃ . (((2 * b₁) + (b₁ * b₉)) + b₁₀) = - 1 ) & ( for b₉ being Nat st b₉ in UsedVx b₄,b₁ holds
b₄ . (b₁ + b₉) <> - 1 ) holds
( ( for b₉ being Vertex of b₆
for b₁₀ being Nat st b₉ <> b₈ & b₉ = b₁₀ & b₅ . (b₁ + b₁₀) <> - 1 holds
ex b₁₁ being FinSequence of NAT ex b₁₂ being oriented Chain of b₆ st
( b₁₁ is_simple_vertex_seq_at b₅,b₁₀,b₁ & ( for b₁₃ being Nat st 1 <= b₁₃ & b₁₃ < len b₁₁ holds
b₁₁ . b₁₃ in UsedVx b₅,b₁ ) & b₁₂ is_oriented_edge_seq_of b₁₁ & b₁₂ is_shortestpath_of b₈,b₉, UsedVx b₅,b₁,b₇ & cost b₁₂,b₇ = b₅ . ((2 * b₁) + b₁₀) & ( not b₉ in UsedVx b₅,b₁ implies b₁₂ islongestInShortestpath UsedVx b₅,b₁,b₈,b₇ ) ) ) & ( for b₉, b₁₀ being Nat st b₅ . (b₁ + b₁₀) = - 1 & 1 <= b₁₀ & b₁₀ <= b₁ & b₉ in UsedVx b₅,b₁ holds
b₃ . (((2 * b₁) + (b₁ * b₉)) + b₁₀) = - 1 ) & ( for b₉ being Nat st b₉ in UsedVx b₅,b₁ holds
b₅ . (b₁ + b₉) <> - 1 ) )

proof end;

theorem Th53: :: GRAPHSP:53

for b₁, b₂ being Nat
for b₃, b₄ being Element of REAL *
for b₅ being oriented finite Graph
for b₆ being Function of the Edges of b₅, Real>=0
for b₇, b₈ being Vertex of b₅ st b₃ is_Input_of_Dijkstra_Alg b₅,b₁,b₆ & b₇ = 1 & 1 <> b₈ & b₈ = b₂ & b₁ >= 1 & b₄ = (DijkstraAlgorithm b₁) . b₃ holds
( the Vertices of b₅ = (UsedVx b₄,b₁) \/ (UnusedVx b₄,b₁) & ( b₈ in UsedVx b₄,b₁ implies ex b₉ being FinSequence of NAT ex b₁₀ being oriented Chain of b₅ st
( b₉ is_simple_vertex_seq_at b₄,b₂,b₁ & b₁₀ is_oriented_edge_seq_of b₉ & b₁₀ is_shortestpath_of b₇,b₈,b₆ & cost b₁₀,b₆ = b₄ . ((2 * b₁) + b₂) ) ) & ( b₈ in UnusedVx b₄,b₁ implies for b₉ being oriented Chain of b₅ holds not b₉ is_orientedpath_of b₇,b₈ ) )

proof end;