Cookies disclaimer

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.

[2018-Nov] Alien

Wow! Alex is retired member of the International SeArch Band for ExtraterrestriaL LifE (short Isabelle), during his lunch time he registered between some noise a clear signal and could obtain the following cleartext:

datatype laoe = Wrosh | kaWum laoe

fun wrotz where
"wrotz (kaWum m) n = kaWum (wrotz m n)"
| "wrotz Wrosh n = n"

fun wrush where
"wrush (kaWum m) n = wrotz n (wrush m n)"
| "wrush Wrosh n = Wrosh"

"wrush k (wrotz m n) =?= wrotz (wrush k m) ((wrush k n)::laoe)"

He somehow sees some patterns in this and is reminded of human mathematics. Shortly before taking his afternoon nap he wonders whether the last sentence is a logical consequence of the before definitions. It seems not clear to neither the aliens who sent the signal nor to Alex whether the last sentence should be correct ...

Can you help him?

i.e.: prove or disprove:

theorem wrotz_wrush_crazy2: "wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe)"

theorem wrotz_wrush_notcrazy2: "~(∀ k m n. wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe))"

Resources

Download Files

Definitions File 

theory Defs
  imports Main
begin 

datatype laoe = Wrosh | kaWum laoe
 
fun wrotz where
  "wrotz (kaWum m) n = kaWum (wrotz m n)"
| "wrotz Wrosh n = n"
 
fun wrush where
  "wrush (kaWum m) n = wrotz n (wrush m n)"
| "wrush Wrosh n = Wrosh"

end

Template File 

theory Submission
  imports Defs
begin
                     
theorem wrotz_wrush_crazy2: "wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe)"
oops

theorem wrotz_wrush_notcrazy2: "~(\<forall>k m n. wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe))"
oops


end

Check File 

theory Check
imports Submission
begin
                     
theorem "wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe)"
by (rule Submission.wrotz_wrush_crazy2)    

theorem "~(\<forall>k m n. wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe))"
by (rule Submission.wrotz_wrush_notcrazy2)    

end
Download Files

Definitions File 

theory Defs
  imports Main
begin 

datatype laoe = Wrosh | kaWum laoe
 
fun wrotz where
  "wrotz (kaWum m) n = kaWum (wrotz m n)"
| "wrotz Wrosh n = n"
 
fun wrush where
  "wrush (kaWum m) n = wrotz n (wrush m n)"
| "wrush Wrosh n = Wrosh"

end

Template File 

theory Submission
  imports Defs
begin
                     
theorem wrotz_wrush_crazy2: "wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe)"
oops

theorem wrotz_wrush_notcrazy2: "~(\<forall>k m n. wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe))"
oops


end

Check File 

theory Check
imports Submission
begin
                     
theorem "wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe)"
by (rule Submission.wrotz_wrush_crazy2)    

theorem "~(\<forall>k m n. wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe))"
by (rule Submission.wrotz_wrush_notcrazy2)    

end
Download Files

Definitions File 

theory Defs
  imports Main
begin 

datatype laoe = Wrosh | kaWum laoe
 
fun wrotz where
  "wrotz (kaWum m) n = kaWum (wrotz m n)"
| "wrotz Wrosh n = n"
 
fun wrush where
  "wrush (kaWum m) n = wrotz n (wrush m n)"
| "wrush Wrosh n = Wrosh"

end

Template File 

theory Submission
  imports Defs
begin
                     
theorem wrotz_wrush_crazy2: "wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe)"
oops

theorem wrotz_wrush_notcrazy2: "~(\<forall>k m n. wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe))"
oops


end

Check File 

theory Check
imports Submission
begin
                     
theorem "wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe)"
by (rule Submission.wrotz_wrush_crazy2)    

theorem "~(\<forall>k m n. wrush k (wrotz m n) = wrotz (wrush k m) ((wrush k n)::laoe))"
by (rule Submission.wrotz_wrush_notcrazy2)    

end
Terms and Conditions