The NecroGame!

Strikingwolf

New Member
Jul 29, 2019
3,709
-26
1
Code:
add_ident : (m : Nat ) -> m = plus m 0
add_ident Z = Refl
add_ident (S k) = rewrite add_ident k in Refl

add_def : (a : Nat) -> (k : Nat) -> S (a + k) = a + (S k)
add_def Z k = Refl
add_def (S j) k = rewrite add_def j k in Refl

add_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
add_commutes Z m = add_ident m
add_commutes (S k) m = rewrite add_commutes k m in add_def m k

add_assoc : (a : Nat) -> (b : Nat) -> (c : Nat) -> a + (b + c) = (a + b) + c
add_assoc Z b c = Refl
add_assoc (S k) b c = rewrite add_assoc k b c in Refl

add_switch : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d)
add_switch a b c d = rewrite add_assoc (a + b) c d in
                     rewrite add_commutes a b in
                     rewrite sym (add_assoc b a c) in
                     rewrite add_commutes b (a + c) in
                     rewrite sym (add_assoc (a + c) b d) in Refl

mult_ident : (n : Nat) -> n = n * 1
mult_ident Z = Refl
mult_ident (S k) = rewrite mult_ident k in Refl

mult_0 : (n : Nat) -> n * 0 = 0
mult_0 Z = Refl
mult_0 (S k) = rewrite mult_0 k in Refl

mult_def : (n : Nat) -> (k : Nat) -> n * (S k) = n + (n * k)
mult_def Z k = Refl
mult_def (S j) k = rewrite mult_def j k in
                   rewrite add_assoc k j (j * k) in
                   rewrite add_commutes k j in
                   rewrite add_assoc j k (j * k) in Refl

mult_commutes : (n : Nat) -> (m : Nat) -> n * m = m * n
mult_commutes Z m = rewrite mult_0 m in Refl
mult_commutes (S k) m = rewrite mult_commutes k m in
                        rewrite mult_def m k in Refl

mult_dist : (a : Nat) -> (b : Nat) -> (c : Nat) -> a * (b + c) = (a * b) + (a * c)
mult_dist Z b c = Refl
mult_dist (S k) b c = rewrite mult_dist k b c in
                      rewrite add_switch b c (k * b) (k * c) in Refl

mult_assoc : (a : Nat) -> (b : Nat) -> (c : Nat) -> a * (b * c) = (a * b) * c
mult_assoc Z b c = Refl
mult_assoc (S k) b c = rewrite mult_assoc k b c in
                       rewrite mult_commutes (b + k * b) c in
                       rewrite mult_dist c b (k * b) in
                       rewrite mult_commutes c b in
                       rewrite mult_commutes c (k * b) in Refl
Idris proofs, because I got bored and wanted to learn idris things
 

Strikingwolf

New Member
Jul 29, 2019
3,709
-26
1
Code:
function System(axiom, rules, parent, count) {
  this.rules = rules;
  this.current = axiom;
  this.parent = parent || this;
  this.count = count || 0;

  this.next = function() {
    var newCurrent = "";
    for (var i = 0; i < this.current.length; i++) {
      var char = this.current[i];
      var newChar = this.rules[char];
      if (newChar != null) {
        newCurrent += newChar;
      } else {
        newCurrent += char;
      }
    }
    return new System(newCurrent, this.rules, this, this.count + 1);
  }

  this.show = function() {
    createP(this.current + ": " + this.count);
  }
}
Because L-systems are fun
 

Celestialphoenix

Too Much Free Time
Nov 9, 2012
3,739
3,208
333
Tartarus.. I mean at work. Same thing really.
So last night I was subject to some of the most intense death glares I'd ever experienced. They never said a word but I could feel the simmering heat boiling off them.
The reason? I tossed a coin before voting out in last night's referendum :p

So next election I'm taking a set of RPG dice and rolling them across the voting booth :)
 
  • Like
Reactions: fowltief

Bigdbigd03

New Member
Jul 29, 2019
159
30
0
Ketchup plain isn't as good as people think


Sent from an iPod 65, illegally talked about because of partnership. iPod 65 teleports through years like Back to the Past (Sequel to Back to the Future except in 2096).
 

Someone Else 37

Forum Addict
Feb 10, 2013
1,878
1,442
168
You can raed tihs txet ptcelerfy wlel, eevn tghouh all the lteerts beewetn the fsirt and lsat are mexid anruod.