class Nat {
    pub. Nat next;
}

class Peano {
    pub. Nat first;
    
    init() { 
        self.first := null;
    }
    
    zero(Nat x) {
        x := null;
    }
        
    succ(Nat x) {
        var Nat z, Nat r;
        
        z := self.first;
        r := null;
        while ( not(eqObj(z, x)) ) {
            r := z;
            z := z.next;
        }
        
        if ( eqObj(r, null) ) {
            Nat.new(r);
            r.next := z;
            self.first := r;
        } else
            skip;
        
        x := r;
        
        end z, r;
    }
    
    pred(Nat x) {
        x := x.next;
    }
    
    add(Nat x, Nat y) {
        if ( eqObj(y, null) ) skip;
        else {
            self.pred(y : x : y);
            self.add(x, y : x, y : x, _);
            self.succ(x : x : x);
        }
    }
    
    mul(Nat x, Nat y) {
        if ( eqObj(y, null) )
            self.zero(x : x : x);
        else {
            var Nat r;
            self.pred(y : x : y);
            self.mul(x, y : x, y : r, _);
            self.add(x, r : x, y : x, _);
            end r;
        }
    }
    
    toInt(Nat x, Int i) {
        if ( eqObj(x, null) )
            i := 0;
        else {
            self.pred(x : x : x);
            self.toInt(x, _ : x, i : _, i);
            i := add(i, 1);
        }
    }
    
    fromInt(int i, Nat x) {
        if ( eqInt(i, 0) )
            x := null;
        else {
            self.fromInt(sub(i, 1), _ : i, x : _, x);
            self.succ(x : x : x);
        }
    }   
}

main {
    Peano p;
    
    Peano.new(p);
    p.init();
    
    var Nat n2, Nat n4, Nat n6, Nat n12, Nat a, Nat b, Int i;
    
    p.fromInt(2, _ : i, x : _, n2);
    p.toInt(n2, _ : x, i : _, i);
    print "n2: ", i;

    p.add(n2, n2 : x, y : n4, _);
    p.toInt(n4, _ : x, i : _, i);
    print "n4: ", i;
    
    p.add(n4, n2 : x, y : n6, _);
    p.toInt(n6, _ : x, i : _, i);
    print "n6: ", i;
    
    p.mul(n6, n2 : x, y : n12, _);
    p.toInt(n12, _ : x, i : _, i);
    print "n12: ", i;
    
    p.mul(n2, n12 : x, y : a, _);
    p.toInt(a, _ : x, i : _, i);
    print "a: ", i;

    p.mul(n4, n6 : x, y : b, _);
    p.toInt(b, _ : x, i : _, i);
    print "b: ", i;
    
    print "eqObj(a, b): ", eqObj(a, b);
    
    end n2, n4, n6, n12, a, b, i;
}