This was my proof of the And Distributes Over Or law.
prfAndDist = startProof(A `And` (B `Or` C))
<-> (Not(Not A) `And` (B `Or` C), dblNeg)
<-> (Not(Not A) `And` Not(Not(B `Or` C)), dblNeg)
<-> (Not(Not A) `And` Not(Not B `And` Not C), deMorgansLawOr)
<-> (Not(Not A `Or` (Not B `And` Not C)), deMorgansLawOr)
<-> (Not((Not A `Or` Not B) `And` (Not A `Or` Not C)), orDistOverAnd)
<-> (Not(Not A `Or` Not B) `Or` Not(Not A `Or` Not C), deMorgansLawAnd)
<-> (Not(Not A `Or` Not B) `Or` (Not(Not A) `Or` Not(Not C)), deMorgansLawOr)
<-> ((Not(Not A) `And` Not(Not B)) `Or` (Not(Not A) `And` Not(Not C)), deMorgansLawOr)
<-> ((A `And` Not(Not B)) `Or` (Not(Not A) `And` Not(Not C)), dblNeg)
<-> ((A `And` B) `Or` (Not(Not A) `And` Not(Not C)), dblNeg)
<-> ((A `And` B) `Or` (A `And` Not(Not C)), dblNeg)
<-> ((A `And` B) `Or` (A `And` C), dblNeg)
Look how long it is.
These are the eror messages I got back from the proof-checker:
The proof is incorrect
Cannot find a substitution into (Not (A `Or` B)) yeilding ((Not ((Not A) `Or` (Not B))) `Or` (Not ((Not A) `Or` (Not C)))):
They have different form
Cannot find a substitution into ((Not A) `And` (Not B)) yeilding ((Not (Not A)) `Or` (Not (Not C))):
They have different form
Terms (Not ((Not A) `Or` (Not C))) and ((Not (Not A)) `Or` (Not (Not C))) cannot be equal:
they do not match the rule and they have different form
Cannot find a substitution into ((Not A) `And` (Not B)) yeilding ((Not ((Not A) `Or` (Not B))) `Or` (Not ((Not A) `Or` (Not C)))):
They have different form
Cannot find a substitution into ((Not A) `And` (Not B)) yeilding (Not ((Not A) `Or` (Not C))):
They have different form
Terms (Not ((Not A) `Or` (Not C))) and ((Not (Not A)) `Or` (Not (Not C))) cannot be equal:
they do not match the rule and they have different form
Again, look at all that. Holy crap, right?
So, I went and checked each line individually in conjunction with the one before and the one after from number three to number seven. Everything checked out. But in staring at it that long, I figured out the problem.
I hadn't done anything wrong; it was a typo. The bolded bit in the proof -- I'd said `Or` when I meant `And`, and it had confused the proof-checker that badly. Lol fail. *shakes head in awe* Thank God I started this early.
- Location:OU
- Mood:
amused
Profile
![[info]](http://l-stat.livejournal.com/img/userinfo.gif)
lonetread- Justin
- My Fanfiction
Comments
Back in senior year of high school, my class was given a final project: to create a program that used linear interpolation to determine the necessary thickness of a wall given various possible materials to comprise it, distance from the target, and an initial level of radiation. Well, my last semester of high school, I had to take AP tests, 8 of them in fact, so I had to rush to complete this project. Well, the night before the project was due, I stayed up the *entire* time trying to get this thing to work. I was almost done, and everything looked like it should work, but it *wasn't*, so I stayed up for a few more hours. Eventually, I collapsed on the couch, and skipped school so I could sleep, hoping that if I was considered sick, I wouldn't be considered late on my project. Later, that massive problem ended up being that I missed a single semi-colon I think, but I was so brought down by spending all of that time and not being able to find that error that I just avoided computer programming for a long while.
The moral of the story? We shouldn't have radiation shielding, and instead trust in the hero(or villain) making powers of radiation.... oh, and computer programming sucks.