[STATEMENT]
lemma path_concatenation_cycle_free:
  assumes "forward_terminating_path x"
      and "backward_terminating_path y"
      and "end_points x = start_points y"
      and "x;1 \<cdot> y\<^sup>T;1 = 0"
    shows "path (x+y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (x + y)
[PROOF STEP]
apply (rule path_concatenation,simp_all add: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; 1 \<cdot> (x\<^sup>T ; 1 + y ; 1) \<cdot> y\<^sup>T ; 1 = 0
[PROOF STEP]
by (metis assms(4) inf.left_commute inf_bot_right inf_commute)