@[instance_reducible]

instance Paramodulator.S_21.instOfNatNodeOfNatNat : OfNat Node 2

Equations

• Paramodulator.S_21.instOfNatNodeOfNatNat = { ofNat := Paramodulator.Node.pair 0 1 }

theorem Paramodulator.S_21.n2_def : 2 = Node.pair 0 1

inductive Paramodulator.S_21.P : Node → Prop

• r0 : P 1
• r1 {a : Node} : P a → P 1
• r2 : P (Node.pair 0 0) → P 0
• r3 {a : Node} : P a → P (Node.pair 0 a)

inductive Paramodulator.S_21.P' : Node → Prop

• r0 : P' 0
• r1 {a : Node} : P' a → P' (Node.pair 0 a)

theorem Paramodulator.S_21.p_eq_p' : P = P'