def Paramodulator.Test.Z : Node

Equations

• Paramodulator.Test.Z = Paramodulator.const 0

def Paramodulator.Test.S : Node

Equations

• Paramodulator.Test.S = Paramodulator.const 1

def Paramodulator.Test.Nat : Node

Equations

• Paramodulator.Test.Nat = Paramodulator.const 2

def Paramodulator.Test.Add : Node

Equations

• Paramodulator.Test.Add = Paramodulator.const 3

inductive Paramodulator.Test.P : Node → Prop

• r0 : P (Nat.pair Z)
• r1 {n : Node} : P (Nat.pair n) → P (Nat.pair (S.pair n))
• r2 {n : Node} : P (Nat.pair n) → P (Add.pair (n.pair (Z.pair n)))
• r3 {n m r : Node} : P (Add.pair (n.pair (m.pair r))) → P (Add.pair (n.pair ((S.pair m).pair (S.pair r))))

def Paramodulator.Test.ofNat (n : ℕ) : Node

Equations

• Paramodulator.Test.ofNat 0 = Paramodulator.Test.Z
• Paramodulator.Test.ofNat n_2.succ = Paramodulator.Test.S.pair (Paramodulator.Test.ofNat n_2)

def Paramodulator.Test.toNat (n : Node) : ℕ

Equations

• Paramodulator.Test.toNat Paramodulator.Node.nil = if Paramodulator.Node.nil = Paramodulator.Test.Z then 0 else 1 + 0
• Paramodulator.Test.toNat (a.pair n_2) = if a.pair n_2 = Paramodulator.Test.Z then 0 else 1 + Paramodulator.Test.toNat n_2

def Paramodulator.Test.IsNat (n : Node) : Prop

Equations

• Paramodulator.Test.IsNat n = Paramodulator.Test.P (Paramodulator.Test.Nat.pair n)

@[simp]

theorem Paramodulator.Test.toNat_Z : toNat Z = 0

@[simp]

theorem Paramodulator.Test.toNat_S {n : Node} : toNat (S.pair n) = toNat n + 1

@[simp]

theorem Paramodulator.Test.toNat_ofNat {n : ℕ} : toNat (ofNat n) = n

@[simp]

theorem Paramodulator.Test.isNat_Z : IsNat Z

@[simp]

theorem Paramodulator.Test.isNat_S {n : Node} : IsNat (S.pair n) ↔ IsNat n

@[simp]

theorem Paramodulator.Test.isNat_ofNat {n : ℕ} : IsNat (ofNat n)

theorem Paramodulator.Test.ofNat_toNat_of {n : Node} (h : IsNat n) : ofNat (toNat n) = n

@[simp]

theorem Paramodulator.Test.ofNat_toNat_iff {n : Node} : ofNat (toNat n) = n ↔ IsNat n

theorem Paramodulator.Test.isNat_iff_exi {n : Node} : IsNat n ↔ ∃ (k : ℕ), ofNat k = n

@[simp]

theorem Paramodulator.Test.P_nat_iff_isNat {n : Node} : P (Nat.pair n) ↔ IsNat n

theorem Paramodulator.Test.Add_iff {n m r : Node} : P (Add.pair (n.pair (m.pair r))) ↔ IsNat n ∧ IsNat m ∧ IsNat r ∧ toNat n + toNat m = toNat r