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.

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))"

Download Files
### Definitions File

### Template File

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

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

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

### Template File

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

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

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

### Template File

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

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

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