I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

`support P = {x. ∃ s1 s2. ( ∀ y. y ≠ x --> s1 y = s2 y) ∧ P s1 ≠ P s2}`

He was really happy, when he could show, that altering a variable not in the support of some function doesnt alter the function.

`x ∉ support Q ==> Q (l(x:=n)) = Q l`

But that was not quite what he wanted. He rather was looking for something else: He wanted to prove that for two states that agree on the support of a function, the function's result for the two states would be equal.

As the lunch break interupted him, he had no more time to think about it. While having coffee he thus posted the question to his fellows, who could not immediately come up with a solution. Could you?

Prove or disprove:

`∀ P. (∀s1 s2. ( ∀ i∈support P. s1 i = s2 i) ==> P s1 = P s2)`

`~ ( ∀ P. ( ∀ s1 s2. ( ∀ i∈support P. s1 i = s2 i) ==> P s1 = P s2))"`

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports Main begin type_synonym vname = string definition support :: "((vname \<Rightarrow> nat) \<Rightarrow> bool) \<Rightarrow> vname set" where "support P = {x. \<exists>s1 s2. (\<forall>y. y \<noteq> x \<longrightarrow> s1 y = s2 y) \<and> P s1 \<noteq> P s2}" lemma lupd: "x \<notin> support Q \<Longrightarrow> Q (l(x:=n)) = Q l" by(simp add: support_def fun_upd_other fun_eq_iff) (metis (no_types, lifting) fun_upd_def) end

theory Submission imports Defs begin lemma prove: "\<forall>P. (\<forall>s1 s2. (\<forall>i\<in>support P. s1 i = s2 i) \<longrightarrow> P s1 = P s2)" sorry (* OR *) lemma disprove: "~ (\<forall>P. (\<forall>s1 s2. (\<forall>i\<in>support P. s1 i = s2 i) \<longrightarrow> P s1 = P s2))" sorry end

theory Check imports Submission begin lemma "~ (\<forall>P. (\<forall>s1 s2. (\<forall>i\<in>Defs.support P. s1 i = s2 i) \<longrightarrow> P s1 = P s2))" apply(fact Submission.disprove) done (* OR *) lemma " (\<forall>P. (\<forall>s1 s2. (\<forall>i\<in>Defs.support P. s1 i = s2 i) \<longrightarrow> P s1 = P s2))" apply(fact Submission.prove) done end

Terms and Conditions