:: GRAPHSP semantic presentation begin theorem :: GRAPHSP:1 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p"))))) & (Bool (Set (Var "p")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ))) ; theorem :: GRAPHSP:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "ii")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "ii"))) & (Bool (Set (Var "ii")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "ii"))) ($#r2_hidden :::"in"::: ) (Set (Var "X")))))) ; theorem :: GRAPHSP:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "ii")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "ii"))) & (Bool (Set (Var "ii")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "ii"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "ii"))))))) ; theorem :: GRAPHSP:4 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "W")) ($#r6_graph_5 :::"is_weight_of"::: ) (Set (Var "G"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "pe")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )))))) ; theorem :: GRAPHSP:5 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))))) "holds" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G"))))) ; theorem :: GRAPHSP:6 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "pe")) "," (Set (Var "qe")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#v1_graph_4 :::"Simple"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "pe")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "qe")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "qe"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "pe")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "pe")) ")" ) ")" ))) & (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "qe")) ($#k1_funct_1 :::"."::: ) (Num 1) ")" ))) ")" )))) ; begin theorem :: GRAPHSP:7 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V"))) "iff" (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v2")) ($#k1_tarski :::"}"::: ) ))) ")" ))))) ; theorem :: GRAPHSP:8 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))) "iff" (Bool (Set (Var "p")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v2")) ($#k1_tarski :::"}"::: ) )) "," (Set (Var "W"))) ")" )))))) ; theorem :: GRAPHSP:9 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool (Set (Var "q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W")))) "holds" (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "p")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "q")) "," (Set (Var "W")) ")" ))))))) ; theorem :: GRAPHSP:10 (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "e2")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "e1")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) & (Bool (Set (Var "e2")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2")))))) ; theorem :: GRAPHSP:11 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "U")) "," (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "U")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "V")))) & (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool "(" "for" (Set (Var "v3")) "," (Set (Var "v4")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v3")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "v4")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) "or" "not" (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v3")) "," (Set (Var "v4"))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))))))) ; theorem :: GRAPHSP:12 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "U")) "," (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "U")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "V")))) & (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool "(" "for" (Set (Var "v3")) "," (Set (Var "v4")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v3")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "v4")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) "or" "not" (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v3")) "," (Set (Var "v4"))) ")" )) ")" ) & (Bool (Set (Var "p")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set (Var "p")) ($#r2_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "U"))))))) ; begin theorem :: GRAPHSP:13 (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "W")) ($#r5_graph_5 :::"is_weight>=0of"::: ) (Set (Var "G"))) & (Bool (Set (Var "P")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v3"))) & (Bool (Set (Var "Q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) "or" "not" (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v2")) "," (Set (Var "v3"))) ")" ) ")" ) & (Bool (Set (Var "P")) ($#r9_graph_5 :::"islongestInShortestpath"::: ) (Set (Var "V")) "," (Set (Var "v1")) "," (Set (Var "W")))) "holds" (Bool (Set (Var "Q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v2")) ($#k1_tarski :::"}"::: ) )) "," (Set (Var "W")))))))) ; theorem :: GRAPHSP:14 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "P")) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set (Var "P")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "v1")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "W")))))))) ; theorem :: GRAPHSP:15 (Bool "for" (Set (Var "e")) "," (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v3")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "P")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "V")) "," (Set (Var "W"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"<>"::: ) (Set (Var "v3"))) & (Bool (Set (Var "Q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k9_finseq_1 :::"*>"::: ) ))) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v2")) "," (Set (Var "v3"))) & (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "V"))) & (Bool "(" "for" (Set (Var "v4")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v4")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "for" (Set (Var "ee")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "ee")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) "or" "not" (Bool (Set (Var "ee")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v4")) "," (Set (Var "v3"))) ")" )) ")" )) "holds" (Bool (Set (Var "Q")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v3")) "," (Set (Set (Var "V")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "v2")) ($#k1_tarski :::"}"::: ) )) "," (Set (Var "W")))))))) ; theorem :: GRAPHSP:16 (Bool "for" (Set (Var "U")) "," (Set (Var "V")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "P")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "U")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "V")))) & (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool "(" "for" (Set (Var "v3")) "," (Set (Var "v4")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "v3")) ($#r2_hidden :::"in"::: ) (Set (Var "U"))) & (Bool (Set (Var "v4")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) "or" "not" (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v3")) "," (Set (Var "v4"))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "P")) ($#r8_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "U")) "," (Set (Var "W"))) "iff" (Bool (Set (Var "P")) ($#r7_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W"))) ")" )))))) ; begin notationlet "f" be ($#m1_hidden :::"Function":::); let "i", "x" be ($#m1_hidden :::"set"::: ) ; synonym "(" "f" "," "i" ")" :::":="::: "x" for "f" :::"+*"::: "(" "i" "," "x" ")" ; end; definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "x" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#m1_subset_1 :::"Real":::); :: original: :::":="::: redefine func "(" "f" "," "x" ")" :::":="::: "r" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "i", "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); let "r" be ($#m1_subset_1 :::"Real":::); func "(" "f" "," "i" ")" :::":="::: "(" "k" "," "r" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) equals :: GRAPHSP:def 1 (Set "(" (Set "(" "(" "f" "," "i" ")" ($#k1_graphsp :::":="::: ) "k" ")" ) "," "k" ")" ($#k1_graphsp :::":="::: ) "r"); end; :: deftheorem defines :::":="::: GRAPHSP:def 1 : (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set "(" (Set (Var "f")) "," (Set (Var "i")) ")" ($#k2_graphsp :::":="::: ) "(" (Set (Var "k")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set "(" "(" (Set (Var "f")) "," (Set (Var "i")) ")" ($#k1_graphsp :::":="::: ) (Set (Var "k")) ")" ) "," (Set (Var "k")) ")" ($#k1_graphsp :::":="::: ) (Set (Var "r"))))))); theorem :: GRAPHSP:17 (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" "(" (Set (Var "f")) "," (Set (Var "i")) ")" ($#k2_graphsp :::":="::: ) "(" (Set (Var "k")) "," (Set (Var "r")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))))) ; theorem :: GRAPHSP:18 (Bool "for" (Set (Var "m")) "," (Set (Var "i")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set (Var "i"))) & (Bool (Set (Var "m")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "f")) "," (Set (Var "i")) ")" ($#k2_graphsp :::":="::: ) "(" (Set (Var "k")) "," (Set (Var "r")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "m"))))))) ; theorem :: GRAPHSP:19 (Bool "for" (Set (Var "k")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" "(" (Set (Var "f")) "," (Set (Var "i")) ")" ($#k2_graphsp :::":="::: ) "(" (Set (Var "k")) "," (Set (Var "r")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "r")))))) ; theorem :: GRAPHSP:20 (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" "(" (Set (Var "f")) "," (Set (Var "i")) ")" ($#k2_graphsp :::":="::: ) "(" (Set (Var "k")) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Const "X")) "," (Set (Const "X")) ")" ); :: original: :::"*"::: redefine func "g" :::"*"::: "f" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "X" ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Const "X")) "," (Set (Const "X")) ")" ); let "g" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "g" -> ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Const "X")) "," (Set (Const "X")) ")" ); func :::"repeat"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "X" ")" ")" ) means :: GRAPHSP:def 2 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_sim1 :::"id"::: ) "X")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_graphsp :::"*"::: ) (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"repeat"::: GRAPHSP:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_graphsp :::"repeat"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_cqc_sim1 :::"id"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_graphsp :::"*"::: ) (Set "(" (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))); theorem :: GRAPHSP:21 (Bool "for" (Set (Var "F")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set (Var "F")) ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k4_graphsp :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: GRAPHSP:22 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set (Var "F")) ($#k3_graphsp :::"*"::: ) (Set (Var "G")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k4_graphsp :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_graphsp :::"."::: ) (Set "(" (Set (Var "G")) ($#k4_graphsp :::"."::: ) (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set (Var "F")) ($#k3_graphsp :::"*"::: ) (Set (Var "G")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_graphsp :::"."::: ) (Set (Var "f")) ")" ) ")" )))))) ; definitionlet "g" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ); let "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); :: original: :::"."::: redefine func "g" :::"."::: "f" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n" be ($#m1_hidden :::"Nat":::); func :::"OuterVx"::: "(" "f" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GRAPHSP:def 3 "{" (Set (Var "i")) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "n") & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) "}" ; end; :: deftheorem defines :::"OuterVx"::: GRAPHSP:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "i")) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) "}" ))); definitionlet "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ); let "g" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n" be ($#m1_hidden :::"Nat":::); assume (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set (Const "f")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Const "g")) ")" ) "," (Set (Const "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; func :::"LifeSpan"::: "(" "f" "," "g" "," "n" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GRAPHSP:def 4 (Bool "(" (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) "f" ")" ) ($#k8_nat_1 :::"."::: ) it ")" ) ($#k6_graphsp :::"."::: ) "g" ")" ) "," "n" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) "f" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_graphsp :::"."::: ) "g" ")" ) "," "n" ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" ); end; :: deftheorem defines :::"LifeSpan"::: GRAPHSP:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set (Var "f")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "g")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k8_graphsp :::"LifeSpan"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "n")) ")" )) "iff" (Bool "(" (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set (Var "f")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "b4")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "g")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set (Var "f")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "g")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "b4")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))))); definitionlet "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"while_do"::: "(" "f" "," "n" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) means :: GRAPHSP:def 5 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set it ($#k6_graphsp :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) "f" ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k8_graphsp :::"LifeSpan"::: ) "(" "f" "," (Set (Var "h")) "," "n" ")" ")" ) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "h")))) ")" ) ")" ); end; :: deftheorem defines :::"while_do"::: GRAPHSP:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_graphsp :::"while_do"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "h")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k6_graphsp :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set (Var "f")) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k8_graphsp :::"LifeSpan"::: ) "(" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "h")))) ")" ) ")" ) ")" )))); begin definitionlet "G" be ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); assume (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G")))) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Const "v1")) "," (Set (Const "v2"))) ")" )) ; func :::"XEdge"::: "(" "v1" "," "v2" ")" -> ($#m1_hidden :::"set"::: ) means :: GRAPHSP:def 6 (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G")) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) "v1" "," "v2") ")" )); end; :: deftheorem defines :::"XEdge"::: GRAPHSP:def 6 : (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" ))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_graphsp :::"XEdge"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" )) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" )) ")" )))); definitionlet "G" be ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "W" be ($#m1_hidden :::"Function":::); func :::"Weight"::: "(" "v1" "," "v2" "," "W" ")" -> ($#m1_hidden :::"set"::: ) equals :: GRAPHSP:def 7 (Set "W" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_graphsp :::"XEdge"::: ) "(" "v1" "," "v2" ")" ")" )) if (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "G")) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) "v1" "," "v2") ")" )) otherwise (Set ($#k1_real_1 :::"-"::: ) (Num 1)); end; :: deftheorem defines :::"Weight"::: GRAPHSP:def 7 : (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" ))) "implies" (Bool (Set ($#k11_graphsp :::"Weight"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_graphsp :::"XEdge"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) ")" ")" ))) ")" & "(" (Bool (Bool "(" "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) "or" "not" (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" ) ")" )) "implies" (Bool (Set ($#k11_graphsp :::"Weight"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ")" )))); definitionlet "G" be ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::); let "v1", "v2" be ($#m1_subset_1 :::"Vertex":::) "of" (Set (Const "G")); let "W" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ); :: original: :::"Weight"::: redefine func :::"Weight"::: "(" "v1" "," "v2" "," "W" ")" -> ($#m1_subset_1 :::"Real":::); end; theorem :: GRAPHSP:23 (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ) "holds" (Bool "(" (Bool (Set ($#k12_graphsp :::"Weight"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "ex" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" )) ")" )))) ; theorem :: GRAPHSP:24 (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ) "holds" (Bool "(" (Bool (Set ($#k12_graphsp :::"Weight"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) "iff" (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) "or" "not" (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2"))) ")" )) ")" )))) ; theorem :: GRAPHSP:25 (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G")))) & (Bool (Set (Var "e")) ($#r1_graph_4 :::"orientedly_joins"::: ) (Set (Var "v1")) "," (Set (Var "v2")))) "holds" (Bool (Set ($#k12_graphsp :::"Weight"::: ) "(" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k1_funct_1 :::"."::: ) (Set (Var "e")))))))) ; begin definitionlet "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"UnusedVx"::: "(" "f" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GRAPHSP:def 8 "{" (Set (Var "i")) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "n") & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) "}" ; end; :: deftheorem defines :::"UnusedVx"::: GRAPHSP:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k13_graphsp :::"UnusedVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "i")) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) "}" ))); definitionlet "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"UsedVx"::: "(" "f" "," "n" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: GRAPHSP:def 9 "{" (Set (Var "i")) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "n") & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) "}" ; end; :: deftheorem defines :::"UsedVx"::: GRAPHSP:def 9 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "i")) where i "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) "}" ))); theorem :: GRAPHSP:26 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k13_graphsp :::"UnusedVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))))) ; registrationlet "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k13_graphsp :::"UnusedVx"::: ) "(" "f" "," "n" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: GRAPHSP:27 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k13_graphsp :::"UnusedVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )))) ; theorem :: GRAPHSP:28 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")))))) ; registrationlet "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k7_graphsp :::"OuterVx"::: ) "(" "f" "," "n" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Argmin"::: "(" "X" "," "f" "," "n" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: GRAPHSP:def 10 (Bool "(" "(" (Bool (Bool "X" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) it) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "X") & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" )) ")" & "(" (Bool (Bool "X" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ); end; :: deftheorem defines :::"Argmin"::: GRAPHSP:def 10 : (Bool "for" (Set (Var "X")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k15_graphsp :::"Argmin"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) "," (Set (Var "n")) ")" )) "iff" (Bool "(" "(" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "b4"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) ")" ) ")" )) ")" & "(" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" )))); theorem :: GRAPHSP:29 (Bool "for" (Set (Var "n")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "j")) ($#r1_hidden :::"="::: ) (Set ($#k15_graphsp :::"Argmin"::: ) "(" (Set "(" ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "f")) "," (Set (Var "n")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ))) ; theorem :: GRAPHSP:30 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k15_graphsp :::"Argmin"::: ) "(" (Set "(" ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))))) ; definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"findmin"::: "n" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) means :: GRAPHSP:def 11 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set it ($#k6_graphsp :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set "(" (Set "(" (Set "(" "n" ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k2_graphsp :::":="::: ) "(" (Set "(" ($#k15_graphsp :::"Argmin"::: ) "(" (Set "(" ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," "n" ")" ")" ) "," (Set (Var "f")) "," "n" ")" ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"findmin"::: GRAPHSP:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k6_graphsp :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "f")) "," (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ($#k2_graphsp :::":="::: ) "(" (Set "(" ($#k15_graphsp :::"Argmin"::: ) "(" (Set "(" ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ")" )) ")" ) ")" ) ")" ))); theorem :: GRAPHSP:31 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n"))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))))) ; theorem :: GRAPHSP:32 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set "(" (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))))) ; theorem :: GRAPHSP:33 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))))) ; theorem :: GRAPHSP:34 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Set "(" (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" )))) ; definitionlet "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n", "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"newpathcost"::: "(" "f" "," "n" "," "k" ")" -> ($#m1_subset_1 :::"Real":::) equals :: GRAPHSP:def 12 (Set (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" "n" ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "n" ($#k8_real_1 :::"*"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" "n" ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) "k" ")" ) ")" )); end; :: deftheorem defines :::"newpathcost"::: GRAPHSP:def 12 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k17_graphsp :::"newpathcost"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "k")) ")" ) ")" ))))); definitionlet "n", "k" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); pred "f" :::"hasBetterPathAt"::: "n" "," "k" means :: GRAPHSP:def 13 (Bool "(" (Bool "(" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) "k" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) "or" (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) "k" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k17_graphsp :::"newpathcost"::: ) "(" "f" "," "n" "," "k" ")" )) ")" ) & (Bool (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "n" ($#k8_real_1 :::"*"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" "n" ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) "k" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) "k") ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ); end; :: deftheorem defines :::"hasBetterPathAt"::: GRAPHSP:def 13 : (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_graphsp :::"hasBetterPathAt"::: ) (Set (Var "n")) "," (Set (Var "k"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) "or" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k17_graphsp :::"newpathcost"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set (Var "k")) ")" )) ")" ) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) ")" ))); definitionlet "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Relax"::: "(" "f" "," "n" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) means :: GRAPHSP:def 14 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f"))) "holds" (Bool "(" "(" (Bool (Bool "n" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) "n"))) "implies" (Bool "(" "(" (Bool (Bool "f" ($#r1_graphsp :::"hasBetterPathAt"::: ) "n" "," (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) "n"))) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" "n" ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" & "(" (Bool (Bool (Bool "not" "f" ($#r1_graphsp :::"hasBetterPathAt"::: ) "n" "," (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) "n")))) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" & "(" (Bool (Bool (Set (Num 2) ($#k4_nat_1 :::"*"::: ) "n") ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 3) ($#k4_nat_1 :::"*"::: ) "n"))) "implies" (Bool "(" "(" (Bool (Bool "f" ($#r1_graphsp :::"hasBetterPathAt"::: ) "n" "," (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" )))) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k17_graphsp :::"newpathcost"::: ) "(" "f" "," "n" "," (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" "f" ($#r1_graphsp :::"hasBetterPathAt"::: ) "n" "," (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ))))) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n") "or" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 3) ($#k4_nat_1 :::"*"::: ) "n")) ")" )) "implies" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Relax"::: GRAPHSP:def 14 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k18_graphsp :::"Relax"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n"))))) "implies" (Bool "(" "(" (Bool (Bool (Set (Var "f")) ($#r1_graphsp :::"hasBetterPathAt"::: ) (Set (Var "n")) "," (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n"))))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "f")) ($#r1_graphsp :::"hasBetterPathAt"::: ) (Set (Var "n")) "," (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set (Var "n")))))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" & "(" (Bool (Bool (Set (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n"))))) "implies" (Bool "(" "(" (Bool (Bool (Set (Var "f")) ($#r1_graphsp :::"hasBetterPathAt"::: ) (Set (Var "n")) "," (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" )))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k17_graphsp :::"newpathcost"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) "," (Set "(" (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ")" )) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "f")) ($#r1_graphsp :::"hasBetterPathAt"::: ) (Set (Var "n")) "," (Set (Set (Var "k")) ($#k7_nat_d :::"-'"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ))))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" & "(" (Bool (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "or" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")))) ")" )) "implies" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ")" ) ")" ) ")" ) ")" )))); definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Relax"::: "n" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) means :: GRAPHSP:def 15 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set it ($#k6_graphsp :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k18_graphsp :::"Relax"::: ) "(" (Set (Var "f")) "," "n" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Relax"::: GRAPHSP:def 15 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k6_graphsp :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k18_graphsp :::"Relax"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" )) ")" ) ")" ) ")" ))); theorem :: GRAPHSP:35 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))))) ; theorem :: GRAPHSP:36 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "or" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Set (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")))) ")" ) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")))))) ; theorem :: GRAPHSP:37 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ))))) ; theorem :: GRAPHSP:38 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k13_graphsp :::"UnusedVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) "," (Set (Var "n")) ")" ) ($#r2_xboole_0 :::"c<"::: ) (Set ($#k13_graphsp :::"UnusedVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) "," (Set (Var "n")) ")" )))) ; theorem :: GRAPHSP:39 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set ($#k15_graphsp :::"Argmin"::: ) "(" (Set "(" ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "g")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "h")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "k")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool (Bool "not" (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ))) ")" ))) ; theorem :: GRAPHSP:40 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; theorem :: GRAPHSP:41 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ))))) ; definitionlet "f", "g" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "m", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "f" "," "g" :::"equal_at"::: "m" "," "n" means :: GRAPHSP:def 16 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "g")) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f")) & (Bool "m" ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n")) "holds" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set "g" ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" ); end; :: deftheorem defines :::"equal_at"::: GRAPHSP:def 16 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_graphsp :::"equal_at"::: ) (Set (Var "m")) "," (Set (Var "n"))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set (Var "k")))) ")" ) ")" ) ")" ))); theorem :: GRAPHSP:42 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Var "f")) "," (Set (Var "f")) ($#r2_graphsp :::"equal_at"::: ) (Set (Var "m")) "," (Set (Var "n"))))) ; theorem :: GRAPHSP:43 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_graphsp :::"equal_at"::: ) (Set (Var "m")) "," (Set (Var "n"))) & (Bool (Set (Var "g")) "," (Set (Var "h")) ($#r2_graphsp :::"equal_at"::: ) (Set (Var "m")) "," (Set (Var "n")))) "holds" (Bool (Set (Var "f")) "," (Set (Var "h")) ($#r2_graphsp :::"equal_at"::: ) (Set (Var "m")) "," (Set (Var "n"))))) ; theorem :: GRAPHSP:44 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f"))) "," (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f"))) ($#r2_graphsp :::"equal_at"::: ) (Set (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ))))) ; theorem :: GRAPHSP:45 (Bool "for" (Set (Var "F")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k8_graphsp :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set ($#k7_graphsp :::"OuterVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set (Var "F")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: GRAPHSP:46 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Var "f")) "," (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f"))) ($#r2_graphsp :::"equal_at"::: ) (Set (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) "," (Set (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ))))) ; theorem :: GRAPHSP:47 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" )) "holds" (Bool "(" (Bool (Num 1) ($#r1_hidden :::"="::: ) (Set ($#k15_graphsp :::"Argmin"::: ) "(" (Set "(" ($#k7_graphsp :::"OuterVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "f")) "," (Set (Var "n")) ")" )) & (Bool (Set ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k14_graphsp :::"UsedVx"::: ) "(" (Set "(" (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Num 1) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")) ")" ) "," (Set (Var "n")) ")" )) ")" ))) ; theorem :: GRAPHSP:48 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "," (Set (Var "h")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Num 1) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k5_graphsp :::"repeat"::: ) (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k8_graphsp :::"LifeSpan"::: ) "(" (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "f")) "," (Set (Var "n")) ")" )) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ))) "holds" (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "h")) "," (Set (Var "n")) ")" )))) ; definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "i", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "p" :::"is_vertex_seq_at"::: "f" "," "i" "," "n" means :: GRAPHSP:def 17 (Bool "(" (Bool (Set "p" ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" )) ($#r1_hidden :::"="::: ) "i") & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p"))) "holds" (Bool (Set "p" ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Set "(" "p" ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "k")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_vertex_seq_at"::: GRAPHSP:def 17 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r3_graphsp :::"is_vertex_seq_at"::: ) (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "n"))) "iff" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k9_real_1 :::"-"::: ) (Set (Var "k")) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ))) ")" ) ")" ) ")" )))); definitionlet "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "i", "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); pred "p" :::"is_simple_vertex_seq_at"::: "f" "," "i" "," "n" means :: GRAPHSP:def 18 (Bool "(" (Bool (Set "p" ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) "p") ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool "p" ($#r3_graphsp :::"is_vertex_seq_at"::: ) "f" "," "i" "," "n") & (Bool "p" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ); end; :: deftheorem defines :::"is_simple_vertex_seq_at"::: GRAPHSP:def 18 : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r4_graphsp :::"is_simple_vertex_seq_at"::: ) (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "n"))) "iff" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "p")) ($#r3_graphsp :::"is_vertex_seq_at"::: ) (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "n"))) & (Bool (Set (Var "p")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ) ")" )))); theorem :: GRAPHSP:49 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r4_graphsp :::"is_simple_vertex_seq_at"::: ) (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "n"))) & (Bool (Set (Var "q")) ($#r4_graphsp :::"is_simple_vertex_seq_at"::: ) (Set (Var "f")) "," (Set (Var "i")) "," (Set (Var "n")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))))) ; definitionlet "G" be ($#l1_graph_1 :::"Graph":::); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G"))); let "vs" be ($#m1_hidden :::"FinSequence":::); pred "p" :::"is_oriented_edge_seq_of"::: "vs" means :: GRAPHSP:def 19 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "vs") ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p"))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set "vs" ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "G") ($#k1_funct_1 :::"."::: ) (Set "(" "p" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set "vs" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"is_oriented_edge_seq_of"::: GRAPHSP:def 19 : (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "vs")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r5_graphsp :::"is_oriented_edge_seq_of"::: ) (Set (Var "vs"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "vs"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "G"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "vs")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ) ")" ) ")" )))); theorem :: GRAPHSP:50 (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r5_graphsp :::"is_oriented_edge_seq_of"::: ) (Set (Var "vs"))) & (Bool (Set (Var "q")) ($#r5_graphsp :::"is_oriented_edge_seq_of"::: ) (Set (Var "vs")))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))))) ; theorem :: GRAPHSP:51 (Bool "for" (Set (Var "G")) "being" ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "vs1")) "," (Set (Var "vs2")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "p")) ($#r5_graphsp :::"is_oriented_edge_seq_of"::: ) (Set (Var "vs1"))) & (Bool (Set (Var "p")) ($#r5_graphsp :::"is_oriented_edge_seq_of"::: ) (Set (Var "vs2"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set (Var "vs1")) ($#r1_hidden :::"="::: ) (Set (Var "vs2")))))) ; begin definitionlet "f" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ); let "G" be ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "W" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ); pred "f" :::"is_Input_of_Dijkstra_Alg"::: "G" "," "n" "," "W" means :: GRAPHSP:def 20 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) "f") ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "n" ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k2_finseq_1 :::"Seg"::: ) "n") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "n")) "holds" (Bool "(" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) "n")) "holds" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "G" (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "holds" (Bool (Set "f" ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) "n" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" "n" ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_graphsp :::"Weight"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," "W" ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_Input_of_Dijkstra_Alg"::: GRAPHSP:def 20 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r6_graphsp :::"is_Input_of_Dijkstra_Alg"::: ) (Set (Var "G")) "," (Set (Var "n")) "," (Set (Var "W"))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Num 3) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) & (Bool "(" "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "k")) "," (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "n")) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_graphsp :::"Weight"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "W")) ")" ))) ")" ) ")" ) ")" ))))); begin definitionlet "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"DijkstraAlgorithm"::: "n" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ) equals :: GRAPHSP:def 21 (Set ($#k9_graphsp :::"while_do"::: ) "(" (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) "n" ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) "n" ")" ) ")" ) "," "n" ")" ); end; :: deftheorem defines :::"DijkstraAlgorithm"::: GRAPHSP:def 21 : (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k20_graphsp :::"DijkstraAlgorithm"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k9_graphsp :::"while_do"::: ) "(" (Set "(" (Set "(" ($#k19_graphsp :::"Relax"::: ) (Set (Var "n")) ")" ) ($#k3_graphsp :::"*"::: ) (Set "(" ($#k16_graphsp :::"findmin"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "n")) ")" ))); begin theorem :: GRAPHSP:52 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k1_numbers :::"REAL"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#v2_graph_1 :::"oriented"::: ) ($#v6_graph_1 :::"finite"::: ) ($#l1_graph_1 :::"Graph":::) (Bool "for" (Set (Var "W")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G"))) "," (Set ($#k8_graph_5 :::"Real>=0"::: ) ) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "f")) ($#r6_graphsp :::"is_Input_of_Dijkstra_Alg"::: ) (Set (Var "G")) "," (Set (Var "n")) "," (Set (Var "W"))) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Num 1) ($#r1_hidden :::"<>"::: ) (Set (Var "v2"))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_graphsp :::"DijkstraAlgorithm"::: ) (Set (Var "n")) ")" ) ($#k6_graphsp :::"."::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k13_graphsp :::"UnusedVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ")" ))) & "(" (Bool (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set ($#k14_graphsp :::"UsedVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ))) "implies" (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "P")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r4_graphsp :::"is_simple_vertex_seq_at"::: ) (Set (Var "g")) "," (Set (Var "i")) "," (Set (Var "n"))) & (Bool (Set (Var "P")) ($#r5_graphsp :::"is_oriented_edge_seq_of"::: ) (Set (Var "p"))) & (Bool (Set (Var "P")) ($#r7_graph_5 :::"is_shortestpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "W"))) & (Bool (Set ($#k10_graph_5 :::"cost"::: ) "(" (Set (Var "P")) "," (Set (Var "W")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")) ")" ))) ")" ))) ")" & "(" (Bool (Bool (Set (Var "v2")) ($#r2_hidden :::"in"::: ) (Set ($#k13_graphsp :::"UnusedVx"::: ) "(" (Set (Var "g")) "," (Set (Var "n")) ")" ))) "implies" (Bool "for" (Set (Var "Q")) "being" ($#v7_graph_1 :::"oriented"::: ) ($#m2_graph_1 :::"Chain"::: ) "of" (Set (Var "G")) "holds" (Bool (Bool "not" (Set (Var "Q")) ($#r1_graph_5 :::"is_orientedpath_of"::: ) (Set (Var "v1")) "," (Set (Var "v2"))))) ")" ")" )))))) ;