The NecroGame!

  • The FTB Forum is now read-only, and is here as an archive. To participate in our community discussions, please join our Discord! https://ftb.team/discord
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
 
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
 
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
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).
 
Because we don't spend enough time playing the game; I can now do it in real life with a functional diamond pickaxe.

f2d579845123d247c205716c5e9732f8.jpg
 
  • Like
Reactions: Bigdbigd03
You can raed tihs txet ptcelerfy wlel, eevn tghouh all the lteerts beewetn the fsirt and lsat are mexid anruod.
 
You must log in or register to reply here.
Top Bottom