@[instance_reducible]

instance Paramodulator.S_61.instOfNatNodeOfNatNat : OfNat Node 2

Equations

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

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

@[instance_reducible]

instance Paramodulator.S_61.instOfNatNodeOfNatNat_1 : OfNat Node 3

Equations

• Paramodulator.S_61.instOfNatNodeOfNatNat_1 = { ofNat := Paramodulator.Node.pair 2 1 }

theorem Paramodulator.S_61.n3_def : 3 = Node.pair 2 1

inductive Paramodulator.S_61.P : Node → Prop

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

inductive Paramodulator.S_61.P' : Node → Prop

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

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