[STATEMENT]
lemma wlog_endpoints_degenerate:
  assumes path_A: "A\<in>\<P>"
      and symmetric_Q: "\<And>a b I. Q I a b \<Longrightarrow> Q I b a"
      and Q_implies_path: "\<And>a b I. \<lbrakk>I\<subseteq>A; Q I a b\<rbrakk> \<Longrightarrow> b\<in>A \<and> a\<in>A"
      and symmetric_P: "\<And>I J. \<lbrakk>\<exists>a b. Q I a b; \<exists>a b. Q J a b; P I J\<rbrakk> \<Longrightarrow> P J I"
      and "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A\<rbrakk>
            \<Longrightarrow> ((a=b \<and> b=c \<and> c=d) \<longrightarrow> P I J) \<and> ((a=b \<and> b\<noteq>c \<and> c=d) \<longrightarrow> P I J)
              \<and> ((a=b \<and> b=c \<and> c\<noteq>d) \<longrightarrow> P I J) \<and> ((a=b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d) \<longrightarrow> P I J)
              \<and> ((a\<noteq>b \<and> b=c \<and> c\<noteq>d \<and> a=d) \<longrightarrow> P I J)
              \<and> (([a;b;c] \<and> a=d) \<longrightarrow> P I J) \<and> (([b;a;c] \<and> a=d) \<longrightarrow> P I J)"
    shows "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
            \<not>(a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d \<and> a\<noteq>c \<and> b\<noteq>d)\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
text \<open>We first extract some of the assumptions of this lemma into the form
  of other WLOG lemmas' assumptions.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have ord1: "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
              [a;b;c] \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; [a;b;c] \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; [a;b;c] \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; [?a;?b;?c] \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have ord2: "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
              [b;a;c] \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; [b;a;c] \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; [b;a;c] \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; [?b;?a;?c] \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have last_case: "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
              a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
using ord1 ord2 wlog_endpoints_degenerate2 symmetric_P symmetric_Q Q_implies_path path_A
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; [?a;?b;?c] \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; [?b;?a;?c] \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J
\<lbrakk>\<And>a b I. ?Q I a b \<Longrightarrow> ?Q I b a; \<And>a b I A. \<lbrakk>I \<subseteq> A; A \<in> \<P>; ?Q I a b\<rbrakk> \<Longrightarrow> b \<in> A \<and> a \<in> A; \<And>I J. \<lbrakk>\<exists>a b. ?Q I a b; \<exists>a b. ?Q J a b; ?P I J\<rbrakk> \<Longrightarrow> ?P J I; \<And>I J a b c d A. \<lbrakk>?Q I a b; ?Q J c d; I \<subseteq> A; J \<subseteq> A; A \<in> \<P>; [a;b;c] \<and> a = d\<rbrakk> \<Longrightarrow> ?P I J; \<And>I J a b c d A. \<lbrakk>?Q I a b; ?Q J c d; I \<subseteq> A; J \<subseteq> A; A \<in> \<P>; [b;a;c] \<and> a = d\<rbrakk> \<Longrightarrow> ?P I J; ?Q ?I ?a ?b; ?Q ?J ?c ?d; ?I \<subseteq> ?A; ?J \<subseteq> ?A; ?A \<in> \<P>; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> ?P ?I ?J
\<lbrakk>\<exists>a b. Q ?I a b; \<exists>a b. Q ?J a b; P ?I ?J\<rbrakk> \<Longrightarrow> P ?J ?I
Q ?I ?a ?b \<Longrightarrow> Q ?I ?b ?a
\<lbrakk>?I \<subseteq> A; Q ?I ?a ?b\<rbrakk> \<Longrightarrow> ?b \<in> A \<and> ?a \<in> A
A \<in> \<P>

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
by (metis abc_sym some_betw)
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
show "\<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I\<subseteq>A; J\<subseteq>A;
            \<not>(a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d \<and> a\<noteq>c \<and> b\<noteq>d)\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
text \<open>Fix the sets on the path, and obtain the assumptions of \<open>wlog_endpoints_degenerate1\<close>.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
fix I J
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
assume asm1: "I\<subseteq>A" "J\<subseteq>A"
[PROOF STATE]
proof (state)
this:
I \<subseteq> A
J \<subseteq> A

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have two: "\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a=b \<and> b=c \<and> c=d\<rbrakk> \<Longrightarrow> P I J"
            "\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a=b \<and> b\<noteq>c \<and> c=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
using \<open>J \<subseteq> A\<close> \<open>I \<subseteq> A\<close> path_A assms(5)
[PROOF STATE]
proof (prove)
using this:
J \<subseteq> A
I \<subseteq> A
A \<in> \<P>
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a = ?b \<and> ?b = ?c \<and> ?c = ?d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have one: "\<And> a b c d. \<lbrakk>Q I a b; Q J c d; a=b \<and> b=c \<and> c\<noteq>d\<rbrakk> \<Longrightarrow> P I J"
          "\<And> a b c d. \<lbrakk>Q I a b; Q J c d; a=b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
using \<open>I \<subseteq> A\<close> \<open>J \<subseteq> A\<close> path_A assms(5)
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> A
J \<subseteq> A
A \<in> \<P>
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
have no: "\<And> a b c d. \<lbrakk>Q I a b; Q J c d; a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
          "\<And> a b c d. \<lbrakk>Q I a b; Q J c d; a\<noteq>b \<and> b=c \<and> c\<noteq>d \<and> a=d\<rbrakk> \<Longrightarrow> P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
using \<open>I \<subseteq> A\<close> \<open>J \<subseteq> A\<close> path_A last_case
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> A
J \<subseteq> A
A \<in> \<P>
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J

goal (1 subgoal):
 1. (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J) &&& (\<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
using \<open>I \<subseteq> A\<close> \<open>J \<subseteq> A\<close> path_A assms(5)
[PROOF STATE]
proof (prove)
using this:
I \<subseteq> A
J \<subseteq> A
A \<in> \<P>
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)

goal (1 subgoal):
 1. \<And>a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
text \<open>Now unwrap the remaining object logic and finish the proof.\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I ?a ?b; Q J ?c ?d; ?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
fix a b c d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
assume asm2: "Q I a b" "Q J c d" "\<not>(a\<noteq>b \<and> b\<noteq>c \<and> c\<noteq>d \<and> a\<noteq>d \<and> a\<noteq>c \<and> b\<noteq>d)"
[PROOF STATE]
proof (state)
this:
Q I a b
Q J c d
\<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)

goal (1 subgoal):
 1. \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; I \<subseteq> A; J \<subseteq> A; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
[PROOF STEP]
show "P I J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P I J
[PROOF STEP]
using two [where a=a and b=b and c=c and d=d]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. P I J
[PROOF STEP]
using one [where a=a and b=b and c=c and d=d]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. P I J
[PROOF STEP]
using no [where a=a and b=b and c=c and d=d]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. P I J
[PROOF STEP]
using wlog_endpoints_degenerate1
        [where I=I and J=J and a=a and b=b and c=c and d=d and P=P and Q=Q]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>\<And>a b I. Q I a b \<Longrightarrow> Q I b a; \<And>I J. \<lbrakk>\<exists>a b. Q I a b; \<exists>a b. Q I a b; P I J\<rbrakk> \<Longrightarrow> P J I; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d \<or> a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d \<or> a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d \<or> a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J; Q I a b; Q J c d; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J

goal (1 subgoal):
 1. P I J
[PROOF STEP]
using asm1 asm2 symmetric_P last_case assms(5) symmetric_Q
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J
\<lbrakk>\<And>a b I. Q I a b \<Longrightarrow> Q I b a; \<And>I J. \<lbrakk>\<exists>a b. Q I a b; \<exists>a b. Q I a b; P I J\<rbrakk> \<Longrightarrow> P J I; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c = d \<or> a = b \<and> b \<noteq> c \<and> c = d\<rbrakk> \<Longrightarrow> P I J; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a = b \<and> b = c \<and> c \<noteq> d \<or> a = b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d\<rbrakk> \<Longrightarrow> P I J; \<And>I J a b c d. \<lbrakk>Q I a b; Q J c d; a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a = d \<or> a \<noteq> b \<and> b = c \<and> c \<noteq> d \<and> a = d\<rbrakk> \<Longrightarrow> P I J; Q I a b; Q J c d; \<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)\<rbrakk> \<Longrightarrow> P I J
I \<subseteq> A
J \<subseteq> A
Q I a b
Q J c d
\<not> (a \<noteq> b \<and> b \<noteq> c \<and> c \<noteq> d \<and> a \<noteq> d \<and> a \<noteq> c \<and> b \<noteq> d)
\<lbrakk>\<exists>a b. Q ?I a b; \<exists>a b. Q ?J a b; P ?I ?J\<rbrakk> \<Longrightarrow> P ?J ?I
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; ?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d\<rbrakk> \<Longrightarrow> P ?I ?J
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A\<rbrakk> \<Longrightarrow> (?a = ?b \<and> ?b = ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c = ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a = ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<longrightarrow> P ?I ?J) \<and> (?a \<noteq> ?b \<and> ?b = ?c \<and> ?c \<noteq> ?d \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?a;?b;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J) \<and> ([?b;?a;?c] \<and> ?a = ?d \<longrightarrow> P ?I ?J)
Q ?I ?a ?b \<Longrightarrow> Q ?I ?b ?a

goal (1 subgoal):
 1. P I J
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
P I J

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>Q ?I ?a ?b; Q ?J ?c ?d; ?I \<subseteq> A; ?J \<subseteq> A; \<not> (?a \<noteq> ?b \<and> ?b \<noteq> ?c \<and> ?c \<noteq> ?d \<and> ?a \<noteq> ?d \<and> ?a \<noteq> ?c \<and> ?b \<noteq> ?d)\<rbrakk> \<Longrightarrow> P ?I ?J

goal:
No subgoals!
[PROOF STEP]
qed