theory QDiaSizeR imports RBG begin (* same bounding-diameter size *) (* crisp relations *) consts SSRdia :: "Rg => Rg => o" LERdia :: "Rg => Rg => o" MinBSpR :: "Rg => Rg => o" BR :: "Rg => Rg => Rg => o" defs MinBSpR_def: "MinBSpR(a,b) == SpR(a) & PR(b,a) & (ALL c. (SpR(c) & PR(b,c) --> LER(a,c)))" SSRdia_def: "SSRdia(a,b) == (EX ca cb. (MinBSpR(ca,a) & MinBSpR(cb,b) & SSR(ca,cb)))" LERdia_def: "LERdia(a,b) == (EX ca cb. (MinBSpR(ca,a) & MinBSpR(cb,b) & LER(ca,cb)))" BR_def: "BR(a,b,c) == SpR(a) & SpR(b) & SpR(c) & (EX sab sbc sac bab bbc bac. (Sum(a,b,sab) & Sum(b,c,sbc) & Sum(a,c,sac) & MinBSpR(bab,sab) & MinBSpR(bbc,sbc) & MinBSpR(bac,sac) & PR(bab,bac) & PR(bbc,bac)))" axioms MinBSpR_exists: "(EX b. MinBSpR(b,a))" PR_and_MinBSpR_and_MinBSpR_imp_PR: "[|PR(a,b);MinBSpR(aa,a);MinBSpR(bb,b)|] ==> PR(aa,bb)" (*MinBSpR_between: "[|MinBSpR(aa,a);PR(a,b);PR(b,aa)|] ==> MinBSpR(aa,b)"*) BR_trans: "[|BR(a,b,w);BR(b,c,w)|] ==> BR(a,b,c)" BR_connect: "[|BR(a,b,w);BR(a,c,w)|] ==> (BR(a,b,c) | BR(a,c,b))" (* theorems for MonBSpR *) theorem MinBSpR_imp_PR: "MinBSpR(a,b) ==> PR(b,a)" apply(unfold MinBSpR_def) apply(auto) done theorem MinBSpR_and_MinBSpR_imp_SSR: "[|MinBSpR(a,c);MinBSpR(b,c)|] ==> SSR(a,b)" apply(unfold MinBSpR_def) apply(rule_tac a="a" and b="b" in LER_and_LER_imp_SSR) apply(auto) done theorem MinBSpR_unique: "[|MinBSpR(a,c);MinBSpR(b,c)|] ==> a=b" apply(rule PR_and_SSR_imp_Id) apply(rule PR_and_MinBSpR_and_MinBSpR_imp_PR [of c c]) apply(rule PR_refl_rule) apply(assumption)+ apply(rule MinBSpR_and_MinBSpR_imp_SSR) apply(auto) done theorem SpR_iff_MinBSpR: "SpR(a) <-> MinBSpR(a,a)" apply(rule iffI) apply(unfold MinBSpR_def) apply(safe) apply(rule PR_refl_rule [of a]) apply(drule_tac a="a" and b="c" in PR_imp_LER) apply(assumption) done theorem EX_SpR_CGR_and_CGR: "(EX c. (SpR(c) & CGR(c,a) & CGR(c,b)))" apply(insert PR_sum) apply(erule_tac x="a" in allE) apply(erule_tac x="b" in allE) apply(clarify) apply(insert MinBSpR_exists) apply(drule allI) apply(erule_tac x="c" in allE) apply(clarify) apply(rule_tac x="ba" in exI) apply(safe) apply(unfold MinBSpR_def) apply(clarify) apply(fold MinBSpR_def) apply(drule_tac a="a" and b="b" and c="c" in Sum_imp_PR_and_PR) apply(clarify) apply(drule_tac a="ba" and b="c" in MinBSpR_imp_PR) apply(drule_tac a="a" and b="c" and c="ba" in PR_trans_rule) apply(assumption) apply(drule_tac a="a" and b="ba" in PR_imp_CGR) apply(rule CGR_sym) apply(clarify) apply(drule_tac a="a" and b="b" and c="c" in Sum_imp_PR_and_PR) apply(clarify) apply(drule_tac a="ba" and b="c" in MinBSpR_imp_PR) apply(drule_tac a="b" and b="c" and c="ba" in PR_trans_rule) apply(assumption) apply(drule_tac a="b" and b="ba" in PR_imp_CGR) apply(rule CGR_sym) apply(clarify) done (* theorems for between *) theorem BR_imp_PR: "BR(a,b,a) ==> PR(b,a)" apply(unfold BR_def) apply(clarify) apply(frule_tac a="a" and b="sac" in Sum_imp_id) apply(clarify) apply(frule_tac a="a" and b="b" in Sum_sym) apply(frule_tac a="b" and b="a" and c="sbc" and d="sab" in Sum_unique) apply(clarify) apply(frule_tac a="bab" and c="sab" and b="bbc" in MinBSpR_unique) apply(clarify) apply(frule_tac a="b" and b="a" and c="sab" in Sum_imp_PR_and_PR) apply(clarify) apply(frule_tac a="bbc" and b="sab" in MinBSpR_imp_PR) apply(frule_tac a="b" and b="sab" and c="bbc" in PR_trans_rule) apply(assumption) apply(frule_tac a="b" and b="bbc" and c="bac" in PR_trans_rule) apply(clarify) apply(simp add: SpR_iff_MinBSpR) apply(frule_tac a="a" and b="bac" and c="a" in MinBSpR_unique) apply(safe) done theorem BR_refl: "[|SpR(a);SpR(b)|] ==> BR(a,a,b)" apply(unfold BR_def) apply(safe) apply(rule_tac x="a" in exI) apply(insert Sum_refl [of a]) apply(insert PR_sum) apply(erule_tac x="a" in allE) apply(erule_tac x="b" in allE) apply(clarify) apply(rule_tac x="c" in exI) apply(rule_tac x="c" in exI) apply(insert MinBSpR_exists [of a]) apply(insert MinBSpR_exists) apply(drule allI) apply(erule_tac x="c" in allE) apply(clarify) apply(rule_tac x="ba" in exI) apply(rule_tac x="baa" in exI) apply(rule_tac x="baa" in exI) apply(safe) apply(drule_tac a="a" and b="b" and c="c" in Sum_imp_PR_and_PR) apply(clarify) apply(drule_tac a="a" and b="c" and aa="ba" and bb="baa" in PR_and_MinBSpR_and_MinBSpR_imp_PR) apply(safe) apply(insert PR_refl) apply(auto) done theorem BR_sym: "BR(a,b,c) ==> BR(c,b,a)" apply(unfold BR_def) apply(clarify) apply(rule_tac x="sbc" in exI) apply(rule_tac x="sab" in exI) apply(rule_tac x="sac" in exI) apply(rule_tac x="bbc" in exI) apply(rule_tac x="bab" in exI) apply(rule_tac x="bac" in exI) apply(safe) apply(insert Sum_sym) apply(auto) done (* theorems for SSRdia and LERdia *) theorem SSRdia_refl: "SSRdia(a,a)" apply(rule ccontr) apply(unfold SSRdia_def) apply(auto) apply(insert MinBSpR_exists [of a]) apply(clarify) apply(erule_tac x="b" in allE) apply(clarify) apply(erule_tac x="b" in allE) apply(safe) apply(insert SSR_refl) apply(erule_tac x="b" in allE) apply(auto) done theorem SSRdia_sym: "SSRdia(a,b) ==> SSRdia(b,a)" apply(unfold SSRdia_def) apply(clarify) apply(rule_tac x="cb" in exI) apply(rule_tac x="ca" in exI) apply(safe) apply(rule_tac a="ca" and b="cb" in SSR_sym) apply(assumption) done theorem SSRdia_trans: "[|SSRdia(a,b);SSRdia(b,c)|] ==> SSRdia(a,c)" apply(unfold SSRdia_def) apply(clarify) apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) apply(assumption) apply(rule_tac x="ca" in exI) apply(rule_tac x="cba" in exI) apply(safe) apply(drule_tac a="ca" and b="cb" and c="cba" in SSR_trans) apply(auto) done theorem LERdia_refl: "LERdia(a,a)" apply(rule ccontr) apply(unfold LERdia_def) apply(auto) apply(insert MinBSpR_exists [of a]) apply(clarify) apply(erule_tac x="b" in allE) apply(clarify) apply(erule_tac x="b" in allE) apply(safe) apply(insert LER_refl) apply(drule allI) apply(erule_tac x="b" in allE) apply(auto) done theorem LERdia_trans: "[|LERdia(a,b);LERdia(b,c)|] ==> LERdia(a,c)" apply(unfold LERdia_def) apply(clarify) apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) apply(assumption) apply(rule_tac x="ca" in exI) apply(rule_tac x="cba" in exI) apply(safe) apply(drule_tac a="ca" and b="cb" and c="cba" in LER_trans) apply(auto) done theorem LERdia_and_LERdia_imp_SSRdia: "[|LERdia(a,b);LERdia(b,a)|] ==> SSRdia(a,b)" apply(unfold LERdia_def,unfold SSRdia_def) apply(clarify) apply(drule_tac a="ca" and b="cba" and c="a" in MinBSpR_unique) apply(assumption) apply(drule_tac a="cb" and b="caa" and c="b" in MinBSpR_unique) apply(assumption) apply(rule_tac x="ca" in exI) apply(rule_tac x="cb" in exI) apply(safe) apply(drule_tac a="cba" and b="caa" in LER_and_LER_imp_SSR) apply(auto) done theorem SSRdia_imp_LERdia_and_LERdia: "SSRdia(a,b) ==> (LERdia(a,b) & LERdia(b,a))" apply(unfold SSRdia_def,unfold LERdia_def) apply(safe) apply(rule_tac x="ca" in exI) apply(rule_tac x="cb" in exI) apply(drule_tac a="ca" and b="cb" in SSR_imp_LER) apply(safe) apply(rule_tac x="cb" in exI) apply(rule_tac x="ca" in exI) apply(drule_tac a="ca" and b="cb" in SSR_sym) apply(drule_tac a="cb" and b="ca" in SSR_imp_LER) apply(safe) done theorem SSRdia_iff_LERdia_and_LERdia: "SSRdia(a,b) <-> (LERdia(a,b) & LERdia(b,a))" apply(rule iffI) apply(drule SSRdia_imp_LERdia_and_LERdia) apply(auto) apply(rule LERdia_and_LERdia_imp_SSRdia) apply(auto) done theorem LERdia_or_LERdia: "(LERdia(a,b) | LERdia(b,a))" apply(insert LER_total) apply(insert MinBSpR_exists [of a]) apply(insert MinBSpR_exists [of b]) apply(clarify) apply(erule_tac x="ba" in allE) apply(erule_tac x="baa" in allE) apply(safe) apply(unfold LERdia_def) apply(auto) done theorem Id_imp_SSRdia: "a=b ==> SSRdia(a,b)" apply(insert SSRdia_refl [of a]) apply(simp) done theorem PR_and_PR_imp_SSRdia: "[|PR(a,b);PR(b,a)|] ==> SSRdia(a,b)" apply(rule Id_imp_SSRdia [of a b]) apply(rule PR_antisym_rule [of a b]) apply(safe) done theorem PR_imp_LERdia: "PR(a,b) ==> LERdia(a,b)" apply(unfold LERdia_def) apply(insert MinBSpR_exists [of a]) apply(insert MinBSpR_exists [of b]) apply(clarify) apply(rule_tac x="ba" in exI) apply(rule_tac x="baa" in exI) apply(safe) apply(drule_tac a="a" and b="b" and aa="ba" and bb="baa" in PR_and_MinBSpR_and_MinBSpR_imp_PR) apply(safe) apply(drule_tac a="ba" and b="baa" in PR_imp_LER) apply(assumption) done theorem LERdia_and_SSRdia_imp_LERdia: "[|LERdia(a,b);SSRdia(b,c)|] ==> LERdia(a,c)" apply(unfold LERdia_def,unfold SSRdia_def) apply(clarify) apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) apply(safe) apply(rule_tac x="ca" in exI) apply(rule_tac x="cba" in exI) apply(safe) apply(drule_tac a="ca" and b="cb" and c="cba" in LER_and_SSR_imp_LER) apply(safe) done theorem SSRdia_and_LERdia_imp_LERdia: "[|SSRdia(a,b);LERdia(b,c)|] ==> LERdia(a,c)" apply(unfold LERdia_def,unfold SSRdia_def) apply(clarify) apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) apply(safe) apply(rule_tac x="ca" in exI) apply(rule_tac x="cba" in exI) apply(safe) apply(drule_tac c="ca" and a="cb" and b="cba" in SSR_and_LER_imp_LER) apply(safe) done theorem SpR_and_SpR_and_SSR_imp_SSRdia: "[|SpR(a);SpR(b);SSR(a,b)|] ==> SSRdia(a,b)" apply(unfold SSRdia_def) apply(rule_tac x="a" in exI) apply(rule_tac x="b" in exI) apply(safe) apply(simp add: SpR_iff_MinBSpR) apply(simp add: SpR_iff_MinBSpR) done theorem SpR_and_SpR_and_SSRdia_imp_SSR: "[|SpR(a);SpR(b);SSRdia(a,b)|] ==> SSR(a,b)" apply(unfold SSRdia_def) apply(clarify) apply(simp add: SpR_iff_MinBSpR) apply(drule_tac a="a" and b="ca" and c="a" in MinBSpR_unique) apply(assumption) apply(drule_tac a="b" and b="cb" and c="b" in MinBSpR_unique) apply(assumption) apply(simp) done theorem SpR_and_SpR_imp_SSR_iff_SSRdia: "[|SpR(a);SpR(b)|] ==> (SSR(a,b) <-> SSRdia(a,b))" apply(safe) apply(rule SpR_and_SpR_and_SSR_imp_SSRdia) apply(auto) apply(rule SpR_and_SpR_and_SSRdia_imp_SSR) apply(auto) done theorem SSRdia_imp_LERdia: "SSRdia(a,b) ==> LERdia(a,b)" apply(unfold LERdia_def) apply(unfold SSRdia_def) apply(clarify) apply(rule_tac x="ca" in exI) apply(rule_tac x="cb" in exI) apply(safe) apply(drule SSR_imp_LER) apply(auto) done (* same bounding-diameter size *) (* vague relations *) consts RSSRdia :: "Rg => Rg => o" NEGRdia :: "Rg => Rg => o" defs RSSRdia_def: "RSSRdia(a,b) == (EX ca cb. (MinBSpR(ca,a) & MinBSpR(cb,b) & RSSR(ca,cb)))" NEGRdia_def: "NEGRdia(a,b) == (EX ca cb. (MinBSpR(ca,a) & MinBSpR(cb,b) & NEGR(ca,cb)))" (* theorems for RSSRdia and NEGdia *) theorem RSSRdia_refl: "RSSRdia(a,a)" apply(unfold RSSRdia_def) apply(insert MinBSpR_exists [of a]) apply(insert MinBSpR_exists [of a]) apply(clarify) apply(rule_tac x="b" in exI) apply(rule_tac x="ba" in exI) apply(safe) apply(drule_tac a="b" and b="ba" and c="a" in MinBSpR_unique) apply(insert RSSR_refl) apply(auto) done theorem RSSRdia_sym: "RSSRdia(a,b) ==> RSSRdia(b,a)" apply(unfold RSSRdia_def) apply(clarify) apply(rule_tac x="cb" in exI) apply(rule_tac x="ca" in exI) apply(safe) apply(rule_tac b="cb" and a="ca" in RSSR_sym) apply(assumption) done (* this cannot be a theorem for the same reason why RSSR_plus is not a theorem for RSSR theorem RSSRdia_plus: "[|Plus(a,c,d1);Plus(b,c,d2);Sym(c,a,b);RSSRdia(a,b)|] ==> RSSRdia(d1,d2)" *) theorem RSSRdia_between: "[|RSSRdia(a,b);LERdia(a,c);LERdia(c,b)|] ==> (RSSRdia(c,a) & RSSRdia(c,b))" apply(unfold RSSRdia_def,unfold LERdia_def) apply(clarify) apply(drule_tac a="ca" and b="caa" and c="a" in MinBSpR_unique) apply(assumption) apply(drule_tac a="cb" and b="cbb" and c="b" in MinBSpR_unique) apply(assumption) apply(drule_tac a="cab" and b="cba" and c="c" in MinBSpR_unique) apply(assumption) apply(safe) apply(rule_tac x="cba" in exI) apply(rule_tac x="caa" in exI) apply(safe) apply(drule_tac a="caa" and b="cbb" and c="cba" in RSSR_between) apply(safe) apply(rule_tac x="cba" in exI) apply(rule_tac x="cbb" in exI) apply(safe) apply(drule_tac a="caa" and b="cbb" and c="cba" in RSSR_between) apply(safe) done theorem SSRdia_and_RSSRdia_imp_RSSRdia: "[|SSRdia(a,b);RSSRdia(b,c)|] ==> RSSRdia(a,c)" apply(unfold SSRdia_def,unfold RSSRdia_def) apply(clarify) apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) apply(assumption) apply(rule_tac x="ca" in exI) apply(rule_tac x="cba" in exI) apply(simp) apply(rule_tac a="ca" and b="cb" and c="cba" in SSR_and_RSSR_imp_RSSR) apply(auto) done theorem RSSRdia_and_SSRdia_imp_RSSRdia: "[|RSSRdia(a,b);SSRdia(b,c)|] ==> RSSRdia(a,c)" apply(unfold SSRdia_def,unfold RSSRdia_def) apply(clarify) apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) apply(assumption) apply(rule_tac x="ca" in exI) apply(rule_tac x="cba" in exI) apply(simp) apply(rule_tac a="ca" and b="cb" and c="cba" in RSSR_and_SSR_imp_RSSR) apply(auto) done theorem SSRdia_imp_RSSRdia: "SSRdia(a,b) ==> RSSRdia(a,b)" apply(insert RSSRdia_refl) apply(insert RSSRdia_and_SSRdia_imp_RSSRdia) apply(auto) done theorem NEGRdia_imp_LERdia: "NEGRdia(a,b) ==> LERdia(a,b)" apply(unfold NEGRdia_def) apply(unfold LERdia_def) apply(clarify) apply(rule_tac x="ca" in exI) apply(rule_tac x="cb" in exI) apply(safe) apply(drule_tac a="ca" and b="cb" in NEGR_imp_LER) apply(safe) done theorem NEGRdia_imp_LERdia_and_notSSRdia: "NEGRdia(a,b) ==> (LERdia(a,b) & ~SSRdia(a,b))" apply(unfold NEGRdia_def) apply(unfold LERdia_def) apply(unfold SSRdia_def) apply(safe) apply(rule_tac x="ca" in exI) apply(rule_tac x="cb" in exI) apply(safe) apply(drule_tac a="ca" and b="cb" in NEGR_imp_LER_and_notSSR) apply(safe) apply(drule_tac a="ca" and b="caa" and c="a" in MinBSpR_unique) apply(assumption) apply(drule_tac a="cb" and b="cba" and c="b" in MinBSpR_unique) apply(assumption) apply(drule_tac a="ca" and b="cb" in NEGR_imp_LER_and_notSSR) apply(safe) done theorem NEGRdia_irrefl: "~NEGRdia(a,a)" apply(unfold NEGRdia_def) apply(safe) apply(drule_tac a="ca" and b="cb" and c="a" in MinBSpR_unique) apply(safe) apply(insert NEGR_irrefl) apply(erule_tac x="cb" in allE) apply(safe) done theorem NEGRdia_assym: "NEGRdia(a,b) ==> ~NEGRdia(b,a)" apply(unfold NEGRdia_def) apply(safe) apply(drule_tac a="ca" and b="cba" and c="a" in MinBSpR_unique) apply(assumption) apply(drule_tac a="cb" and b="caa" and c="b" in MinBSpR_unique) apply(safe) apply(drule_tac a="cba" and b="caa" in NEGR_assym) apply(safe) done theorem LERdia_and_NEGRdia_imp_NEGRdia: "[|LERdia(a,b);NEGRdia(b,c)|] ==> NEGRdia(a,c)" apply(unfold NEGRdia_def) apply(unfold LERdia_def) apply(clarify) apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) apply(safe) apply(rule_tac x="ca" in exI) apply(rule_tac x="cba" in exI) apply(safe) apply(drule_tac a="ca" and b="cb" and c="cba" in LER_and_NEGR_imp_NEGR) apply(safe) done theorem NEGRdia_and_LERdia_imp_NEGRdia: "[|NEGRdia(a,b);LERdia(b,c)|] ==> NEGRdia(a,c)" apply(unfold NEGRdia_def) apply(unfold LERdia_def) apply(clarify) apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) apply(safe) apply(rule_tac x="ca" in exI) apply(rule_tac x="cba" in exI) apply(safe) apply(drule_tac a="ca" and b="cb" and c="cba" in NEGR_and_LER_imp_NEGR) apply(safe) done theorem SSRdia_and_NEGRdia_imp_NEGRdia: "[|SSRdia(a,b);NEGRdia(b,c)|] ==> NEGRdia(a,c)" apply(drule SSRdia_imp_LERdia) apply(drule LERdia_and_NEGRdia_imp_NEGRdia) apply(auto) done theorem NEGRdia_SSRdia_imp_NEGRdia: "[|NEGRdia(a,b);SSRdia(b,c)|] ==> NEGRdia(a,c)" apply(drule SSRdia_imp_LERdia [of b c]) apply(drule NEGRdia_and_LERdia_imp_NEGRdia) apply(auto) done theorem NEGRdia_trans: "[|NEGRdia(a,b);NEGRdia(b,c)|] ==> NEGRdia(a,c)" apply(drule NEGRdia_imp_LERdia) apply(drule LERdia_and_NEGRdia_imp_NEGRdia) apply(auto) done theorem PR_and_NEGRdia_imp_NEGRdia: "[|PR(a,b);NEGRdia(b,c)|] ==> NEGRdia(a,c)" apply(drule PR_imp_LERdia) apply(drule LERdia_and_NEGRdia_imp_NEGRdia) apply(auto) done theorem NEGRdia_PR_imp_NEGRdia: "[|NEGRdia(a,b);PR(b,c)|] ==> NEGRdia(a,c)" apply(drule PR_imp_LERdia [of b c]) apply(drule NEGRdia_and_LERdia_imp_NEGRdia) apply(auto) done theorem SpR_and_SpR_and_RSSR_imp_RSSRdia: "[|SpR(a);SpR(b);RSSR(a,b)|] ==> RSSRdia(a,b)" apply(unfold RSSRdia_def) apply(rule_tac x="a" in exI) apply(rule_tac x="b" in exI) apply(safe) apply(simp add: SpR_iff_MinBSpR) apply(simp add: SpR_iff_MinBSpR) done theorem SpR_and_SpR_and_RSSRdia_imp_RSSR: "[|SpR(a);SpR(b);RSSRdia(a,b)|] ==> RSSR(a,b)" apply(unfold RSSRdia_def) apply(clarify) apply(simp add: SpR_iff_MinBSpR) apply(drule_tac a="a" and b="ca" and c="a" in MinBSpR_unique) apply(assumption) apply(drule_tac a="b" and b="cb" and c="b" in MinBSpR_unique) apply(assumption) apply(simp) done theorem SpR_and_SpR_imp_RSSR_iff_RSSRdia: "[|SpR(a);SpR(b)|] ==> (RSSR(a,b) <-> RSSRdia(a,b))" apply(safe) apply(rule SpR_and_SpR_and_RSSR_imp_RSSRdia) apply(auto) apply(rule SpR_and_SpR_and_RSSRdia_imp_RSSR) apply(auto) done end
theorem MinBSpR_imp_PR:
MinBSpR(a, b) ==> PR(b, a)
theorem MinBSpR_and_MinBSpR_imp_SSR:
[| MinBSpR(a, c); MinBSpR(b, c) |] ==> SSR(a, b)
theorem MinBSpR_unique:
[| MinBSpR(a, c); MinBSpR(b, c) |] ==> a = b
theorem SpR_iff_MinBSpR:
SpR(a) <-> MinBSpR(a, a)
theorem EX_SpR_CGR_and_CGR:
∃c. SpR(c) ∧ CGR(c, a) ∧ CGR(c, b)
theorem BR_imp_PR:
BR(a, b, a) ==> PR(b, a)
theorem BR_refl:
[| SpR(a); SpR(b) |] ==> BR(a, a, b)
theorem BR_sym:
BR(a, b, c) ==> BR(c, b, a)
theorem SSRdia_refl:
SSRdia(a, a)
theorem SSRdia_sym:
SSRdia(a, b) ==> SSRdia(b, a)
theorem SSRdia_trans:
[| SSRdia(a, b); SSRdia(b, c) |] ==> SSRdia(a, c)
theorem LERdia_refl:
LERdia(a, a)
theorem LERdia_trans:
[| LERdia(a, b); LERdia(b, c) |] ==> LERdia(a, c)
theorem LERdia_and_LERdia_imp_SSRdia:
[| LERdia(a, b); LERdia(b, a) |] ==> SSRdia(a, b)
theorem SSRdia_imp_LERdia_and_LERdia:
SSRdia(a, b) ==> LERdia(a, b) ∧ LERdia(b, a)
theorem SSRdia_iff_LERdia_and_LERdia:
SSRdia(a, b) <-> LERdia(a, b) ∧ LERdia(b, a)
theorem LERdia_or_LERdia:
LERdia(a, b) ∨ LERdia(b, a)
theorem Id_imp_SSRdia:
a = b ==> SSRdia(a, b)
theorem PR_and_PR_imp_SSRdia:
[| PR(a, b); PR(b, a) |] ==> SSRdia(a, b)
theorem PR_imp_LERdia:
PR(a, b) ==> LERdia(a, b)
theorem LERdia_and_SSRdia_imp_LERdia:
[| LERdia(a, b); SSRdia(b, c) |] ==> LERdia(a, c)
theorem SSRdia_and_LERdia_imp_LERdia:
[| SSRdia(a, b); LERdia(b, c) |] ==> LERdia(a, c)
theorem SpR_and_SpR_and_SSR_imp_SSRdia:
[| SpR(a); SpR(b); SSR(a, b) |] ==> SSRdia(a, b)
theorem SpR_and_SpR_and_SSRdia_imp_SSR:
[| SpR(a); SpR(b); SSRdia(a, b) |] ==> SSR(a, b)
theorem SpR_and_SpR_imp_SSR_iff_SSRdia:
[| SpR(a); SpR(b) |] ==> SSR(a, b) <-> SSRdia(a, b)
theorem SSRdia_imp_LERdia:
SSRdia(a, b) ==> LERdia(a, b)
theorem RSSRdia_refl:
RSSRdia(a, a)
theorem RSSRdia_sym:
RSSRdia(a, b) ==> RSSRdia(b, a)
theorem RSSRdia_between:
[| RSSRdia(a, b); LERdia(a, c); LERdia(c, b) |]
==> RSSRdia(c, a) ∧ RSSRdia(c, b)
theorem SSRdia_and_RSSRdia_imp_RSSRdia:
[| SSRdia(a, b); RSSRdia(b, c) |] ==> RSSRdia(a, c)
theorem RSSRdia_and_SSRdia_imp_RSSRdia:
[| RSSRdia(a, b); SSRdia(b, c) |] ==> RSSRdia(a, c)
theorem SSRdia_imp_RSSRdia:
SSRdia(a, b) ==> RSSRdia(a, b)
theorem NEGRdia_imp_LERdia:
NEGRdia(a, b) ==> LERdia(a, b)
theorem NEGRdia_imp_LERdia_and_notSSRdia:
NEGRdia(a, b) ==> LERdia(a, b) ∧ ¬ SSRdia(a, b)
theorem NEGRdia_irrefl:
¬ NEGRdia(a, a)
theorem NEGRdia_assym:
NEGRdia(a, b) ==> ¬ NEGRdia(b, a)
theorem LERdia_and_NEGRdia_imp_NEGRdia:
[| LERdia(a, b); NEGRdia(b, c) |] ==> NEGRdia(a, c)
theorem NEGRdia_and_LERdia_imp_NEGRdia:
[| NEGRdia(a, b); LERdia(b, c) |] ==> NEGRdia(a, c)
theorem SSRdia_and_NEGRdia_imp_NEGRdia:
[| SSRdia(a, b); NEGRdia(b, c) |] ==> NEGRdia(a, c)
theorem NEGRdia_SSRdia_imp_NEGRdia:
[| NEGRdia(a, b); SSRdia(b, c) |] ==> NEGRdia(a, c)
theorem NEGRdia_trans:
[| NEGRdia(a, b); NEGRdia(b, c) |] ==> NEGRdia(a, c)
theorem PR_and_NEGRdia_imp_NEGRdia:
[| PR(a, b); NEGRdia(b, c) |] ==> NEGRdia(a, c)
theorem NEGRdia_PR_imp_NEGRdia:
[| NEGRdia(a, b); PR(b, c) |] ==> NEGRdia(a, c)
theorem SpR_and_SpR_and_RSSR_imp_RSSRdia:
[| SpR(a); SpR(b); RSSR(a, b) |] ==> RSSRdia(a, b)
theorem SpR_and_SpR_and_RSSRdia_imp_RSSR:
[| SpR(a); SpR(b); RSSRdia(a, b) |] ==> RSSR(a, b)
theorem SpR_and_SpR_imp_RSSR_iff_RSSRdia:
[| SpR(a); SpR(b) |] ==> RSSR(a, b) <-> RSSRdia(a, b)