[STATEMENT]
lemma transitive_linorder_matrix:
  fixes f :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  shows "matrix_idempotent_semiring.transitive f \<longleftrightarrow> (\<forall>i j k . f (i,k) \<le> f (i,j) \<or> f (k,j) \<le> f (i,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
have "matrix_idempotent_semiring.transitive f \<longleftrightarrow> (\<forall>i j . (\<Squnion>\<^sub>k f (i,k) * f (k,j)) \<le> f (i,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j. sup_monoid.sum (\<lambda>k. f (i, k) * f (k, j)) {k. True} \<le> f (i, j))
[PROOF STEP]
by (simp add: times_matrix_def less_eq_matrix_def)
[PROOF STATE]
proof (state)
this:
matrix_idempotent_semiring.transitive f = (\<forall>i j. sup_monoid.sum (\<lambda>k. f (i, k) * f (k, j)) {k. True} \<le> f (i, j))

goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_idempotent_semiring.transitive f = (\<forall>i j. sup_monoid.sum (\<lambda>k. f (i, k) * f (k, j)) {k. True} \<le> f (i, j))

goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>i j k . f (i,k) * f (k,j) \<le> f (i,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i j. sup_monoid.sum (\<lambda>k. f (i, k) * f (k, j)) {k. True} \<le> f (i, j)) = (\<forall>i j k. f (i, k) * f (k, j) \<le> f (i, j))
[PROOF STEP]
by (simp add: lub_sum_iff)
[PROOF STATE]
proof (state)
this:
(\<forall>i j. sup_monoid.sum (\<lambda>k. f (i, k) * f (k, j)) {k. True} \<le> f (i, j)) = (\<forall>i j k. f (i, k) * f (k, j) \<le> f (i, j))

goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>i j. sup_monoid.sum (\<lambda>k. f (i, k) * f (k, j)) {k. True} \<le> f (i, j)) = (\<forall>i j k. f (i, k) * f (k, j) \<le> f (i, j))

goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
have "... \<longleftrightarrow> (\<forall>i j k . f (i,k) \<le> f (i,j) \<or> f (k,j) \<le> f (i,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i j k. f (i, k) * f (k, j) \<le> f (i, j)) = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
using inf_less_eq
[PROOF STATE]
proof (prove)
using this:
(?x \<sqinter> ?y \<le> ?z) = (?x \<le> ?z \<or> ?y \<le> ?z)

goal (1 subgoal):
 1. (\<forall>i j k. f (i, k) * f (k, j) \<le> f (i, j)) = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<forall>i j k. f (i, k) * f (k, j) \<le> f (i, j)) = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))

goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))

goal (1 subgoal):
 1. matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
matrix_idempotent_semiring.transitive f = (\<forall>i j k. f (i, k) \<le> f (i, j) \<or> f (k, j) \<le> f (i, j))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coreflexive_comp_linorder_matrix:
  fixes f g :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_idempotent_semiring.coreflexive f"
    shows "(f \<odot> g) (i,j) = f (i,i) \<sqinter> g (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
have 1: "\<forall>k . i \<noteq> k \<longrightarrow> f (i,k) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. i \<noteq> k \<longrightarrow> f (i, k) = bot
[PROOF STEP]
using assms coreflexive_linorder_matrix
[PROOF STATE]
proof (prove)
using this:
matrix_idempotent_semiring.coreflexive f
matrix_idempotent_semiring.coreflexive ?f = (\<forall>i j. i \<noteq> j \<longrightarrow> ?f (i, j) = bot)

goal (1 subgoal):
 1. \<forall>k. i \<noteq> k \<longrightarrow> f (i, k) = bot
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>k. i \<noteq> k \<longrightarrow> f (i, k) = bot

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
have "(\<Squnion>\<^sub>k f (i,k)) = f (i,i) \<squnion> (\<Squnion>\<^bsub>k\<in>UNIV-{i}\<^esub> f (i,k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, i) \<squnion> sup_monoid.sum (\<lambda>k. f (i, k)) (UNIV - {i})
[PROOF STEP]
by (metis (no_types) UNIV_def brouwer.inf_bot_right finite_UNIV insert_def sup_monoid.sum.insert_remove)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, i) \<squnion> sup_monoid.sum (\<lambda>k. f (i, k)) (UNIV - {i})

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
hence 2: "(\<Squnion>\<^sub>k f (i,k)) = f (i,i)"
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, i) \<squnion> sup_monoid.sum (\<lambda>k. f (i, k)) (UNIV - {i})

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, i)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, i) \<squnion> sup_monoid.sum (\<lambda>k. f (i, k)) (UNIV - {i})
\<forall>k. i \<noteq> k \<longrightarrow> f (i, k) = bot

goal (1 subgoal):
 1. sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, i)
[PROOF STEP]
by (metis (no_types) linorder_finite_sup_selective sup_not_bot)
[PROOF STATE]
proof (state)
this:
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, i)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
have "(f \<odot> g) (i,j) = (f \<odot> mtop \<otimes> g) (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> g) (i, j) = (f \<odot> mtop \<otimes> g) (i, j)
[PROOF STEP]
by (metis assms matrix_stone_relation_algebra.coreflexive_comp_top_inf)
[PROOF STATE]
proof (state)
this:
(f \<odot> g) (i, j) = (f \<odot> mtop \<otimes> g) (i, j)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<odot> g) (i, j) = (f \<odot> mtop \<otimes> g) (i, j)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
have "... = (\<Squnion>\<^sub>k f (i,k)) \<sqinter> g (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> mtop \<otimes> g) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<sqinter> g (i, j)
[PROOF STEP]
by (metis inf_matrix_def comp_top_linorder_matrix)
[PROOF STATE]
proof (state)
this:
(f \<odot> mtop \<otimes> g) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<sqinter> g (i, j)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<odot> g) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<sqinter> g (i, j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f \<odot> g) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<sqinter> g (i, j)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(f \<odot> g) (i, j) = sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} \<sqinter> g (i, j)
sup_monoid.sum (\<lambda>k. f (i, k)) {k. True} = f (i, i)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f \<odot> g) (i, j) = f (i, i) \<sqinter> g (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_coreflexive_linorder_matrix:
  fixes f g :: "('a::finite,'b::linorder_stone_relation_algebra_expansion) square"
  assumes "matrix_idempotent_semiring.coreflexive g"
    shows "(f \<odot> g) (i,j) = f (i,j) \<sqinter> g (j,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
have "(f \<odot> g) (i,j) = ((f \<odot> g)\<^sup>t) (j,i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<odot> g) (i, j) = ((f \<odot> g)\<^sup>t) (j, i)
[PROOF STEP]
by (simp add: conv_matrix_def)
[PROOF STATE]
proof (state)
this:
(f \<odot> g) (i, j) = ((f \<odot> g)\<^sup>t) (j, i)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(f \<odot> g) (i, j) = ((f \<odot> g)\<^sup>t) (j, i)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
have "... = (g \<odot> f\<^sup>t) (j,i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f \<odot> g)\<^sup>t) (j, i) = (g \<odot> f\<^sup>t) (j, i)
[PROOF STEP]
by (simp add: assms matrix_stone_relation_algebra.conv_dist_comp matrix_stone_relation_algebra.coreflexive_symmetric)
[PROOF STATE]
proof (state)
this:
((f \<odot> g)\<^sup>t) (j, i) = (g \<odot> f\<^sup>t) (j, i)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((f \<odot> g)\<^sup>t) (j, i) = (g \<odot> f\<^sup>t) (j, i)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
have "... = g (j,j) \<sqinter> (f\<^sup>t) (j,i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<odot> f\<^sup>t) (j, i) = g (j, j) \<sqinter> (f\<^sup>t) (j, i)
[PROOF STEP]
by (simp add: assms coreflexive_comp_linorder_matrix)
[PROOF STATE]
proof (state)
this:
(g \<odot> f\<^sup>t) (j, i) = g (j, j) \<sqinter> (f\<^sup>t) (j, i)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(g \<odot> f\<^sup>t) (j, i) = g (j, j) \<sqinter> (f\<^sup>t) (j, i)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
have "... = f (i,j) \<sqinter> g (j,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (j, j) \<sqinter> (f\<^sup>t) (j, i) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
by (metis (no_types, lifting) conv_def old.prod.case conv_matrix_def inf_commute)
[PROOF STATE]
proof (state)
this:
g (j, j) \<sqinter> (f\<^sup>t) (j, i) = f (i, j) \<sqinter> g (j, j)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)

goal (1 subgoal):
 1. (f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f \<odot> g) (i, j) = f (i, j) \<sqinter> g (j, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUIDl_eq[simp,intro!]: "eqButUIDl uid uidl uidl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid uidl uidl
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUIDl_sym:
assumes "eqButUIDl uid uidl uidl1"
shows "eqButUIDl uid uidl1 uidl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid uidl1 uidl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDl uid uidl uidl1

goal (1 subgoal):
 1. eqButUIDl uid uidl1 uidl
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUIDl_trans:
assumes "eqButUIDl uid uidl uidl1" and "eqButUIDl uid uidl1 uidl2"
shows "eqButUIDl uid uidl uidl2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid uidl uidl2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDl uid uidl uidl1
eqButUIDl uid uidl1 uidl2

goal (1 subgoal):
 1. eqButUIDl uid uidl uidl2
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUIDl_remove1_cong:
assumes "eqButUIDl uid uidl uidl1"
shows "eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
have "remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)
[PROOF STEP]
by (simp add: remove1_commute)
[PROOF STATE]
proof (state)
this:
remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
remove1 uid (remove1 uid' uidl) = remove1 uid' (remove1 uid uidl)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
have "\<dots> = remove1 uid' (remove1 uid uidl1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remove1 uid' (remove1 uid uidl) = remove1 uid' (remove1 uid uidl1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDl uid uidl uidl1

goal (1 subgoal):
 1. remove1 uid' (remove1 uid uidl) = remove1 uid' (remove1 uid uidl1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
remove1 uid' (remove1 uid uidl) = remove1 uid' (remove1 uid uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
remove1 uid' (remove1 uid uidl) = remove1 uid' (remove1 uid uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
have "\<dots> = remove1 uid (remove1 uid' uidl1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remove1 uid' (remove1 uid uidl1) = remove1 uid (remove1 uid' uidl1)
[PROOF STEP]
by (simp add: remove1_commute)
[PROOF STATE]
proof (state)
this:
remove1 uid' (remove1 uid uidl1) = remove1 uid (remove1 uid' uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
remove1 uid (remove1 uid' uidl) = remove1 uid (remove1 uid' uidl1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
remove1 uid (remove1 uid' uidl) = remove1 uid (remove1 uid' uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eqButUIDl uid (remove1 uid' uidl) (remove1 uid' uidl1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUIDl_snoc_cong:
assumes "eqButUIDl uid uidl uidl1"
and "uid' \<in>\<in> uidl \<longleftrightarrow> uid' \<in>\<in> uidl1"
shows "eqButUIDl uid (uidl ## uid') (uidl1 ## uid')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl uid (uidl ## uid') (uidl1 ## uid')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDl uid uidl uidl1
(uid' \<in>\<in> uidl) = (uid' \<in>\<in> uidl1)

goal (1 subgoal):
 1. eqButUIDl uid (uidl ## uid') (uidl1 ## uid')
[PROOF STEP]
by (auto simp add: remove1_append remove1_idem)


[STATEMENT]
lemma eqButUIDf_eeq[simp,intro!]: "eqButUIDf frds frds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf frds frds
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds UID1) \<and> eqButUIDl UID1 (frds UID2) (frds UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds uid)
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUIDf_sym:
assumes "eqButUIDf frds frds1" shows "eqButUIDf frds1 frds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf frds1 frds
[PROOF STEP]
using assms eqButUIDl_sym
[PROOF STATE]
proof (prove)
using this:
eqButUIDf frds frds1
eqButUIDl ?uid ?uidl ?uidl1.0 \<Longrightarrow> eqButUIDl ?uid ?uidl1.0 ?uidl

goal (1 subgoal):
 1. eqButUIDf frds1 frds
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)
eqButUIDl ?uid ?uidl ?uidl1.0 \<Longrightarrow> eqButUIDl ?uid ?uidl1.0 ?uidl

goal (1 subgoal):
 1. eqButUIDl UID2 (frds1 UID1) (frds UID1) \<and> eqButUIDl UID1 (frds1 UID2) (frds UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds1 uid = frds uid)
[PROOF STEP]
by presburger


[STATEMENT]
lemma eqButUIDf_trans:
assumes "eqButUIDf frds frds1" and "eqButUIDf frds1 frds2"
shows "eqButUIDf frds frds2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf frds frds2
[PROOF STEP]
using assms eqButUIDl_trans
[PROOF STATE]
proof (prove)
using this:
eqButUIDf frds frds1
eqButUIDf frds1 frds2
\<lbrakk>eqButUIDl ?uid ?uidl ?uidl1.0; eqButUIDl ?uid ?uidl1.0 ?uidl2.0\<rbrakk> \<Longrightarrow> eqButUIDl ?uid ?uidl ?uidl2.0

goal (1 subgoal):
 1. eqButUIDf frds frds2
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)
eqButUIDl UID2 (frds1 UID1) (frds2 UID1) \<and> eqButUIDl UID1 (frds1 UID2) (frds2 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds1 uid = frds2 uid)
\<lbrakk>eqButUIDl ?uid ?uidl ?uidl1.0; eqButUIDl ?uid ?uidl1.0 ?uidl2.0\<rbrakk> \<Longrightarrow> eqButUIDl ?uid ?uidl ?uidl2.0

goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds2 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds2 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds2 uid)
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUIDf_cong:
assumes "eqButUIDf frds frds1"
and "uid = UID1 \<Longrightarrow> eqButUIDl UID2 uu uu1"
and "uid = UID2 \<Longrightarrow> eqButUIDl UID1 uu uu1"
and "uid \<noteq> UID1 \<Longrightarrow> uid \<noteq> UID2 \<Longrightarrow> uu = uu1"
shows "eqButUIDf (frds (uid := uu)) (frds1(uid := uu1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDf (frds(uid := uu)) (frds1(uid := uu1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDf frds frds1
uid = UID1 \<Longrightarrow> eqButUIDl UID2 uu uu1
uid = UID2 \<Longrightarrow> eqButUIDl UID1 uu uu1
\<lbrakk>uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. eqButUIDf (frds(uid := uu)) (frds1(uid := uu1))
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)
uid = UID1 \<Longrightarrow> eqButUIDl UID2 uu uu1
uid = UID2 \<Longrightarrow> eqButUIDl UID1 uu uu1
\<lbrakk>uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. eqButUIDl UID2 ((frds(uid := uu)) UID1) ((frds1(uid := uu1)) UID1) \<and> eqButUIDl UID1 ((frds(uid := uu)) UID2) ((frds1(uid := uu1)) UID2) \<and> (\<forall>uida. uida \<noteq> UID1 \<and> uida \<noteq> UID2 \<longrightarrow> (frds(uid := uu)) uida = (frds1(uid := uu1)) uida)
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUIDf_eqButUIDl:
assumes "eqButUIDf frds frds1"
shows "eqButUIDl UID2 (frds UID1) (frds1 UID1)"
  and "eqButUIDl UID1 (frds UID2) (frds1 UID2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds1 UID1) &&& eqButUIDl UID1 (frds UID2) (frds1 UID2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUIDf frds frds1

goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds1 UID1) &&& eqButUIDl UID1 (frds UID2) (frds1 UID2)
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)

goal (1 subgoal):
 1. eqButUIDl UID2 (frds UID1) (frds1 UID1) &&& eqButUIDl UID1 (frds UID2) (frds1 UID2)
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUIDf_not_UID:
"\<lbrakk>eqButUIDf frds frds1; uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> frds uid = frds1 uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqButUIDf frds frds1; uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> frds uid = frds1 uid
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid); uid \<noteq> UID1; uid \<noteq> UID2\<rbrakk> \<Longrightarrow> frds uid = frds1 uid
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUIDf_not_UID':
assumes eq1: "eqButUIDf frds frds1"
and uid: "(uid,uid') \<notin> {(UID1,UID2), (UID2,UID1)}"
shows "uid \<in>\<in> frds uid' \<longleftrightarrow> uid \<in>\<in> frds1 uid'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
from uid
[PROOF STATE]
proof (chain)
picking this:
(uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)}
[PROOF STEP]
have "(uid' = UID1 \<and> uid \<noteq> UID2)
               \<or> (uid' = UID2 \<and> uid \<noteq> UID1)
               \<or> (uid' \<notin> {UID1,UID2})" (is "?u1 \<or> ?u2 \<or> ?n12")
[PROOF STATE]
proof (prove)
using this:
(uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)}

goal (1 subgoal):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<or> uid' = UID2 \<and> uid \<noteq> UID1 \<or> uid' \<notin> {UID1, UID2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uid' = UID1 \<and> uid \<noteq> UID2 \<or> uid' = UID2 \<and> uid \<noteq> UID1 \<or> uid' \<notin> {UID1, UID2}

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' = UID1 \<and> uid \<noteq> UID2 \<or> uid' = UID2 \<and> uid \<noteq> UID1 \<or> uid' \<notin> {UID1, UID2}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2 \<or> uid' = UID2 \<and> uid \<noteq> UID1 \<or> uid' \<notin> {UID1, UID2}

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 3. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
assume "?u1"
[PROOF STATE]
proof (state)
this:
uid' = UID1 \<and> uid \<noteq> UID2

goal (3 subgoals):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 3. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
uid' = UID1 \<and> uid \<noteq> UID2

goal (3 subgoals):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 3. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' = UID1 \<and> uid \<noteq> UID2
[PROOF STEP]
have "uid \<in>\<in> remove1 UID2 (frds uid') \<longleftrightarrow> uid \<in>\<in> remove1 UID2 (frds1 uid')"
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2
eqButUIDf frds frds1

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))

goal (3 subgoals):
 1. uid' = UID1 \<and> uid \<noteq> UID2 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 3. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
uid' = UID1 \<and> uid \<noteq> UID2
(uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uid' = UID1 \<and> uid \<noteq> UID2
(uid \<in>\<in> remove1 UID2 (frds uid')) = (uid \<in>\<in> remove1 UID2 (frds1 uid'))

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')

goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
assume "?u2"
[PROOF STATE]
proof (state)
this:
uid' = UID2 \<and> uid \<noteq> UID1

goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
uid' = UID2 \<and> uid \<noteq> UID1

goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' = UID2 \<and> uid \<noteq> UID1
[PROOF STEP]
have "uid \<in>\<in> remove1 UID1 (frds uid') \<longleftrightarrow> uid \<in>\<in> remove1 UID1 (frds1 uid')"
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<and> uid \<noteq> UID1

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<and> uid \<noteq> UID1
eqButUIDf frds frds1

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<and> uid \<noteq> UID1
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)

goal (1 subgoal):
 1. (uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))

goal (2 subgoals):
 1. uid' = UID2 \<and> uid \<noteq> UID1 \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
 2. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
uid' = UID2 \<and> uid \<noteq> UID1
(uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uid' = UID2 \<and> uid \<noteq> UID1
(uid \<in>\<in> remove1 UID1 (frds uid')) = (uid \<in>\<in> remove1 UID1 (frds1 uid'))

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')

goal (1 subgoal):
 1. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
assume "?n12"
[PROOF STATE]
proof (state)
this:
uid' \<notin> {UID1, UID2}

goal (1 subgoal):
 1. uid' \<notin> {UID1, UID2} \<Longrightarrow> (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
uid' \<notin> {UID1, UID2}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
uid' \<notin> {UID1, UID2}

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
using eq1
[PROOF STATE]
proof (prove)
using this:
uid' \<notin> {UID1, UID2}
eqButUIDf frds frds1

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
unfolding eqButUIDf_def
[PROOF STATE]
proof (prove)
using this:
uid' \<notin> {UID1, UID2}
eqButUIDl UID2 (frds UID1) (frds1 UID1) \<and> eqButUIDl UID1 (frds UID2) (frds1 UID2) \<and> (\<forall>uid. uid \<noteq> UID1 \<and> uid \<noteq> UID2 \<longrightarrow> frds uid = frds1 uid)

goal (1 subgoal):
 1. (uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(uid \<in>\<in> frds uid') = (uid \<in>\<in> frds1 uid')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqButUID12_eeq[simp,intro!]: "eqButUID12 freq freq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 freq freq
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq uid uid'
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUID12_sym:
assumes "eqButUID12 freq freq1" shows "eqButUID12 freq1 freq"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 freq1 freq
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUID12 freq freq1

goal (1 subgoal):
 1. eqButUID12 freq1 freq
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
using this:
\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq1 uid uid'

goal (1 subgoal):
 1. \<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq1 uid uid' = freq uid uid'
[PROOF STEP]
by presburger


[STATEMENT]
lemma eqButUID12_trans:
assumes "eqButUID12 freq freq1" and "eqButUID12 freq1 freq2"
shows "eqButUID12 freq freq2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 freq freq2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUID12 freq freq1
eqButUID12 freq1 freq2

goal (1 subgoal):
 1. eqButUID12 freq freq2
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
using this:
\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq1 uid uid'
\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq1 uid uid' = freq2 uid uid'

goal (1 subgoal):
 1. \<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq2 uid uid'
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUID12_cong:
assumes "eqButUID12 freq freq1"
(*and "uid = UID1 \<Longrightarrow> eqButUID2 uu uu1"*)
and "\<not> (uid,uid') \<in> {(UID1,UID2), (UID2,UID1)} \<Longrightarrow> uu = uu1"
shows "eqButUID12 (fun_upd2 freq uid uid' uu) (fun_upd2 freq1 uid uid' uu1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID12 (fun_upd2 freq uid uid' uu) (fun_upd2 freq1 uid uid' uu1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUID12 freq freq1
(uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)} \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. eqButUID12 (fun_upd2 freq uid uid' uu) (fun_upd2 freq1 uid uid' uu1)
[PROOF STEP]
unfolding eqButUID12_def fun_upd2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq1 uid uid'
(uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)} \<Longrightarrow> uu = uu1

goal (1 subgoal):
 1. \<forall>uida uid'a. if (uida, uid'a) \<in> {(UID1, UID2), (UID2, UID1)} then True else (if uid = uida \<and> uid' = uid'a then uu else freq uida uid'a) = (if uid = uida \<and> uid' = uid'a then uu1 else freq1 uida uid'a)
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUID12_not_UID:
"\<lbrakk>eqButUID12 freq freq1; \<not> (uid,uid') \<in> {(UID1,UID2), (UID2,UID1)}\<rbrakk> \<Longrightarrow> freq uid uid' = freq1 uid uid'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqButUID12 freq freq1; (uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)}\<rbrakk> \<Longrightarrow> freq uid uid' = freq1 uid uid'
[PROOF STEP]
unfolding eqButUID12_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>uid uid'. if (uid, uid') \<in> {(UID1, UID2), (UID2, UID1)} then True else freq uid uid' = freq1 uid uid'; (uid, uid') \<notin> {(UID1, UID2), (UID2, UID1)}\<rbrakk> \<Longrightarrow> freq uid uid' = freq1 uid uid'
[PROOF STEP]
by (auto split: if_splits)


[STATEMENT]
lemma eqButUID_refl[simp,intro!]: "eqButUID s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admin s = admin s \<and> pendingUReqs s = pendingUReqs s \<and> userReq s = userReq s \<and> userIDs s = userIDs s \<and> user s = user s \<and> pass s = pass s \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s) \<and> eqButUID12 (friendReq s) (friendReq s) \<and> eqButUIDf (friendIDs s) (friendIDs s) \<and> postIDs s = postIDs s \<and> admin s = admin s \<and> post s = post s \<and> vis s = vis s \<and> owner s = owner s \<and> pendingSApiReqs s = pendingSApiReqs s \<and> sApiReq s = sApiReq s \<and> serverApiIDs s = serverApiIDs s \<and> serverPass s = serverPass s \<and> outerPostIDs s = outerPostIDs s \<and> outerPost s = outerPost s \<and> outerVis s = outerVis s \<and> outerOwner s = outerOwner s \<and> sentOuterFriendIDs s = sentOuterFriendIDs s \<and> recvOuterFriendIDs s = recvOuterFriendIDs s \<and> pendingCApiReqs s = pendingCApiReqs s \<and> cApiReq s = cApiReq s \<and> clientApiIDs s = clientApiIDs s \<and> clientPass s = clientPass s \<and> sharedWith s = sharedWith s
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUID_sym[sym]:
assumes "eqButUID s s1" shows "eqButUID s1 s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s1 s
[PROOF STEP]
using assms eqButUIDf_sym eqButUID12_sym
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
eqButUIDf ?frds ?frds1.0 \<Longrightarrow> eqButUIDf ?frds1.0 ?frds
eqButUID12 ?freq ?freq1.0 \<Longrightarrow> eqButUID12 ?freq1.0 ?freq

goal (1 subgoal):
 1. eqButUID s1 s
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
using this:
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1
eqButUIDf ?frds ?frds1.0 \<Longrightarrow> eqButUIDf ?frds1.0 ?frds
eqButUID12 ?freq ?freq1.0 \<Longrightarrow> eqButUID12 ?freq1.0 ?freq

goal (1 subgoal):
 1. admin s1 = admin s \<and> pendingUReqs s1 = pendingUReqs s \<and> userReq s1 = userReq s \<and> userIDs s1 = userIDs s \<and> user s1 = user s \<and> pass s1 = pass s \<and> eqButUIDf (pendingFReqs s1) (pendingFReqs s) \<and> eqButUID12 (friendReq s1) (friendReq s) \<and> eqButUIDf (friendIDs s1) (friendIDs s) \<and> postIDs s1 = postIDs s \<and> admin s1 = admin s \<and> post s1 = post s \<and> vis s1 = vis s \<and> owner s1 = owner s \<and> pendingSApiReqs s1 = pendingSApiReqs s \<and> sApiReq s1 = sApiReq s \<and> serverApiIDs s1 = serverApiIDs s \<and> serverPass s1 = serverPass s \<and> outerPostIDs s1 = outerPostIDs s \<and> outerPost s1 = outerPost s \<and> outerVis s1 = outerVis s \<and> outerOwner s1 = outerOwner s \<and> sentOuterFriendIDs s1 = sentOuterFriendIDs s \<and> recvOuterFriendIDs s1 = recvOuterFriendIDs s \<and> pendingCApiReqs s1 = pendingCApiReqs s \<and> cApiReq s1 = cApiReq s \<and> clientApiIDs s1 = clientApiIDs s \<and> clientPass s1 = clientPass s \<and> sharedWith s1 = sharedWith s
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUID_trans[trans]:
assumes "eqButUID s s1" and "eqButUID s1 s2" shows "eqButUID s s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s2
[PROOF STEP]
using assms eqButUIDf_trans eqButUID12_trans
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1
eqButUID s1 s2
\<lbrakk>eqButUIDf ?frds ?frds1.0; eqButUIDf ?frds1.0 ?frds2.0\<rbrakk> \<Longrightarrow> eqButUIDf ?frds ?frds2.0
\<lbrakk>eqButUID12 ?freq ?freq1.0; eqButUID12 ?freq1.0 ?freq2.0\<rbrakk> \<Longrightarrow> eqButUID12 ?freq ?freq2.0

goal (1 subgoal):
 1. eqButUID s s2
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
using this:
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1
admin s1 = admin s2 \<and> pendingUReqs s1 = pendingUReqs s2 \<and> userReq s1 = userReq s2 \<and> userIDs s1 = userIDs s2 \<and> user s1 = user s2 \<and> pass s1 = pass s2 \<and> eqButUIDf (pendingFReqs s1) (pendingFReqs s2) \<and> eqButUID12 (friendReq s1) (friendReq s2) \<and> eqButUIDf (friendIDs s1) (friendIDs s2) \<and> postIDs s1 = postIDs s2 \<and> admin s1 = admin s2 \<and> post s1 = post s2 \<and> vis s1 = vis s2 \<and> owner s1 = owner s2 \<and> pendingSApiReqs s1 = pendingSApiReqs s2 \<and> sApiReq s1 = sApiReq s2 \<and> serverApiIDs s1 = serverApiIDs s2 \<and> serverPass s1 = serverPass s2 \<and> outerPostIDs s1 = outerPostIDs s2 \<and> outerPost s1 = outerPost s2 \<and> outerVis s1 = outerVis s2 \<and> outerOwner s1 = outerOwner s2 \<and> sentOuterFriendIDs s1 = sentOuterFriendIDs s2 \<and> recvOuterFriendIDs s1 = recvOuterFriendIDs s2 \<and> pendingCApiReqs s1 = pendingCApiReqs s2 \<and> cApiReq s1 = cApiReq s2 \<and> clientApiIDs s1 = clientApiIDs s2 \<and> clientPass s1 = clientPass s2 \<and> sharedWith s1 = sharedWith s2
\<lbrakk>eqButUIDf ?frds ?frds1.0; eqButUIDf ?frds1.0 ?frds2.0\<rbrakk> \<Longrightarrow> eqButUIDf ?frds ?frds2.0
\<lbrakk>eqButUID12 ?freq ?freq1.0; eqButUID12 ?freq1.0 ?freq2.0\<rbrakk> \<Longrightarrow> eqButUID12 ?freq ?freq2.0

goal (1 subgoal):
 1. admin s = admin s2 \<and> pendingUReqs s = pendingUReqs s2 \<and> userReq s = userReq s2 \<and> userIDs s = userIDs s2 \<and> user s = user s2 \<and> pass s = pass s2 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s2) \<and> eqButUID12 (friendReq s) (friendReq s2) \<and> eqButUIDf (friendIDs s) (friendIDs s2) \<and> postIDs s = postIDs s2 \<and> admin s = admin s2 \<and> post s = post s2 \<and> vis s = vis s2 \<and> owner s = owner s2 \<and> pendingSApiReqs s = pendingSApiReqs s2 \<and> sApiReq s = sApiReq s2 \<and> serverApiIDs s = serverApiIDs s2 \<and> serverPass s = serverPass s2 \<and> outerPostIDs s = outerPostIDs s2 \<and> outerPost s = outerPost s2 \<and> outerVis s = outerVis s2 \<and> outerOwner s = outerOwner s2 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s2 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s2 \<and> pendingCApiReqs s = pendingCApiReqs s2 \<and> cApiReq s = cApiReq s2 \<and> clientApiIDs s = clientApiIDs s2 \<and> clientPass s = clientPass s2 \<and> sharedWith s = sharedWith s2
[PROOF STEP]
by metis


[STATEMENT]
lemma eqButUID_stateSelectors:
assumes "eqButUID s s1"
shows "admin s = admin s1"
"pendingUReqs s = pendingUReqs s1" "userReq s = userReq s1"
"userIDs s = userIDs s1" "user s = user s1" "pass s = pass s1"
"eqButUIDf (pendingFReqs s) (pendingFReqs s1)"
"eqButUID12 (friendReq s) (friendReq s1)"
"eqButUIDf (friendIDs s) (friendIDs s1)"

"postIDs s = postIDs s1"
"post s = post s1" "vis s = vis s1"
"owner s = owner s1"

"pendingSApiReqs s = pendingSApiReqs s1" "sApiReq s = sApiReq s1"
"serverApiIDs s = serverApiIDs s1" "serverPass s = serverPass s1"
"outerPostIDs s = outerPostIDs s1" "outerPost s = outerPost s1" "outerVis s = outerVis s1"
"outerOwner s = outerOwner s1"
"sentOuterFriendIDs s = sentOuterFriendIDs s1"
"recvOuterFriendIDs s = recvOuterFriendIDs s1"

"pendingCApiReqs s = pendingCApiReqs s1" "cApiReq s = cApiReq s1"
"clientApiIDs s = clientApiIDs s1" "clientPass s = clientPass s1"
"sharedWith s = sharedWith s1"

"IDsOK s = IDsOK s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((admin s = admin s1 &&& pendingUReqs s = pendingUReqs s1 &&& userReq s = userReq s1) &&& (userIDs s = userIDs s1 &&& user s = user s1) &&& pass s = pass s1 &&& eqButUIDf (pendingFReqs s) (pendingFReqs s1)) &&& (eqButUID12 (friendReq s) (friendReq s1) &&& eqButUIDf (friendIDs s) (friendIDs s1) &&& postIDs s = postIDs s1) &&& (post s = post s1 &&& vis s = vis s1) &&& owner s = owner s1 &&& pendingSApiReqs s = pendingSApiReqs s1) &&& ((sApiReq s = sApiReq s1 &&& serverApiIDs s = serverApiIDs s1 &&& serverPass s = serverPass s1) &&& (outerPostIDs s = outerPostIDs s1 &&& outerPost s = outerPost s1) &&& outerVis s = outerVis s1 &&& outerOwner s = outerOwner s1) &&& ((sentOuterFriendIDs s = sentOuterFriendIDs s1 &&& recvOuterFriendIDs s = recvOuterFriendIDs s1) &&& pendingCApiReqs s = pendingCApiReqs s1 &&& cApiReq s = cApiReq s1) &&& (clientApiIDs s = clientApiIDs s1 &&& clientPass s = clientPass s1) &&& sharedWith s = sharedWith s1 &&& IDsOK s = IDsOK s1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqButUID s s1

goal (1 subgoal):
 1. (((admin s = admin s1 &&& pendingUReqs s = pendingUReqs s1 &&& userReq s = userReq s1) &&& (userIDs s = userIDs s1 &&& user s = user s1) &&& pass s = pass s1 &&& eqButUIDf (pendingFReqs s) (pendingFReqs s1)) &&& (eqButUID12 (friendReq s) (friendReq s1) &&& eqButUIDf (friendIDs s) (friendIDs s1) &&& postIDs s = postIDs s1) &&& (post s = post s1 &&& vis s = vis s1) &&& owner s = owner s1 &&& pendingSApiReqs s = pendingSApiReqs s1) &&& ((sApiReq s = sApiReq s1 &&& serverApiIDs s = serverApiIDs s1 &&& serverPass s = serverPass s1) &&& (outerPostIDs s = outerPostIDs s1 &&& outerPost s = outerPost s1) &&& outerVis s = outerVis s1 &&& outerOwner s = outerOwner s1) &&& ((sentOuterFriendIDs s = sentOuterFriendIDs s1 &&& recvOuterFriendIDs s = recvOuterFriendIDs s1) &&& pendingCApiReqs s = pendingCApiReqs s1 &&& cApiReq s = cApiReq s1) &&& (clientApiIDs s = clientApiIDs s1 &&& clientPass s = clientPass s1) &&& sharedWith s = sharedWith s1 &&& IDsOK s = IDsOK s1
[PROOF STEP]
unfolding eqButUID_def IDsOK_def[abs_def]
[PROOF STATE]
proof (prove)
using this:
admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1

goal (1 subgoal):
 1. (((admin s = admin s1 &&& pendingUReqs s = pendingUReqs s1 &&& userReq s = userReq s1) &&& (userIDs s = userIDs s1 &&& user s = user s1) &&& pass s = pass s1 &&& eqButUIDf (pendingFReqs s) (pendingFReqs s1)) &&& (eqButUID12 (friendReq s) (friendReq s1) &&& eqButUIDf (friendIDs s) (friendIDs s1) &&& postIDs s = postIDs s1) &&& (post s = post s1 &&& vis s = vis s1) &&& owner s = owner s1 &&& pendingSApiReqs s = pendingSApiReqs s1) &&& ((sApiReq s = sApiReq s1 &&& serverApiIDs s = serverApiIDs s1 &&& serverPass s = serverPass s1) &&& (outerPostIDs s = outerPostIDs s1 &&& outerPost s = outerPost s1) &&& outerVis s = outerVis s1 &&& outerOwner s = outerOwner s1) &&& ((sentOuterFriendIDs s = sentOuterFriendIDs s1 &&& recvOuterFriendIDs s = recvOuterFriendIDs s1) &&& pendingCApiReqs s = pendingCApiReqs s1 &&& cApiReq s = cApiReq s1) &&& (clientApiIDs s = clientApiIDs s1 &&& clientPass s = clientPass s1) &&& sharedWith s = sharedWith s1 &&& (\<lambda>uIDs pIDs saID_pIDs_s caIDs. list_all (\<lambda>uID. uID \<in>\<in> userIDs s) uIDs \<and> list_all (\<lambda>pID. pID \<in>\<in> postIDs s) pIDs \<and> list_all (\<lambda>(aID, pIDs). aID \<in>\<in> serverApiIDs s \<and> list_all (\<lambda>pID. pID \<in>\<in> outerPostIDs s aID) pIDs) saID_pIDs_s \<and> list_all (\<lambda>aID. aID \<in>\<in> clientApiIDs s) caIDs) = (\<lambda>uIDs pIDs saID_pIDs_s caIDs. list_all (\<lambda>uID. uID \<in>\<in> userIDs s1) uIDs \<and> list_all (\<lambda>pID. pID \<in>\<in> postIDs s1) pIDs \<and> list_all (\<lambda>(aID, pIDs). aID \<in>\<in> serverApiIDs s1 \<and> list_all (\<lambda>pID. pID \<in>\<in> outerPostIDs s1 aID) pIDs) saID_pIDs_s \<and> list_all (\<lambda>aID. aID \<in>\<in> clientApiIDs s1) caIDs)
[PROOF STEP]
by auto


[STATEMENT]
lemma eqButUID_eqButUID2:
"eqButUID s s1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqButUID s s1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)
[PROOF STEP]
using eqButUIDf_eqButUIDl
[PROOF STATE]
proof (prove)
using this:
eqButUIDf ?frds ?frds1.0 \<Longrightarrow> eqButUIDl UID2 (?frds UID1) (?frds1.0 UID1)
eqButUIDf ?frds ?frds1.0 \<Longrightarrow> eqButUIDl UID1 (?frds UID2) (?frds1.0 UID2)

goal (1 subgoal):
 1. admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1 \<Longrightarrow> eqButUIDl UID2 (friendIDs s UID1) (friendIDs s1 UID1)
[PROOF STEP]
by (smt eqButUIDf_eqButUIDl eqButUIDl.simps)


[STATEMENT]
lemma eqButUID_not_UID:
"eqButUID s s1 \<Longrightarrow> uid \<noteq> UID \<Longrightarrow> post s uid = post s1 uid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eqButUID s s1; uid \<noteq> UID\<rbrakk> \<Longrightarrow> post s uid = post s1 uid
[PROOF STEP]
unfolding eqButUID_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>admin s = admin s1 \<and> pendingUReqs s = pendingUReqs s1 \<and> userReq s = userReq s1 \<and> userIDs s = userIDs s1 \<and> user s = user s1 \<and> pass s = pass s1 \<and> eqButUIDf (pendingFReqs s) (pendingFReqs s1) \<and> eqButUID12 (friendReq s) (friendReq s1) \<and> eqButUIDf (friendIDs s) (friendIDs s1) \<and> postIDs s = postIDs s1 \<and> admin s = admin s1 \<and> post s = post s1 \<and> vis s = vis s1 \<and> owner s = owner s1 \<and> pendingSApiReqs s = pendingSApiReqs s1 \<and> sApiReq s = sApiReq s1 \<and> serverApiIDs s = serverApiIDs s1 \<and> serverPass s = serverPass s1 \<and> outerPostIDs s = outerPostIDs s1 \<and> outerPost s = outerPost s1 \<and> outerVis s = outerVis s1 \<and> outerOwner s = outerOwner s1 \<and> sentOuterFriendIDs s = sentOuterFriendIDs s1 \<and> recvOuterFriendIDs s = recvOuterFriendIDs s1 \<and> pendingCApiReqs s = pendingCApiReqs s1 \<and> cApiReq s = cApiReq s1 \<and> clientApiIDs s = clientApiIDs s1 \<and> clientPass s = clientPass s1 \<and> sharedWith s = sharedWith s1; uid \<noteq> UID\<rbrakk> \<Longrightarrow> post s uid = post s1 uid
[PROOF STEP]
by auto