[STATEMENT]
lemma shortestPath_transfer [transfer_rule]:
  assumes [transfer_rule]: "right_total G"
    and [transfer_rule]: "(G ===> (=)) \<alpha>e \<alpha>e2"
    and [transfer_rule]: "(G ===> (=)) \<alpha>n \<alpha>n2"
    and [transfer_rule]: "(G ===> (=)) invar invar2"
    and [transfer_rule]: "(G ===> (=)) inEdges' inEdges2"
    and [transfer_rule]: "(G ===> (=)) Entry Entry2"
  shows "(G ===> (=)) shortestPath (graph_Entry.shortestPath \<alpha>n2 invar2 inEdges2 Entry2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G ===> (=)) shortestPath (graph_Entry.shortestPath \<alpha>n2 invar2 inEdges2 Entry2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (G ===> (=)) shortestPath (graph_Entry.shortestPath \<alpha>n2 invar2 inEdges2 Entry2)
[PROOF STEP]
interpret gE2: graph_Entry \<alpha>e2 \<alpha>n2 invar2 inEdges2 Entry2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_Entry \<alpha>e2 \<alpha>n2 invar2 inEdges2 Entry2
[PROOF STEP]
by transfer' unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (G ===> (=)) shortestPath gE2.shortestPath
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G ===> (=)) shortestPath gE2.shortestPath
[PROOF STEP]
unfolding shortestPath_def [abs_def] gE2.shortestPath_def [abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G ===> (=)) (\<lambda>g n. LEAST l. \<exists>ns. length ns = l \<and> g \<turnstile> Entry g-ns\<rightarrow>n) (\<lambda>g n. LEAST l. \<exists>ns. length ns = l \<and> gE2.path2 g (Entry2 g) ns n)
[PROOF STEP]
by transfer_prover
[PROOF STATE]
proof (state)
this:
(G ===> (=)) shortestPath gE2.shortestPath

goal:
No subgoals!
[PROOF STEP]
qed