###### Cookies disclaimer

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.

# 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```

Terms and Conditions