@[instance_reducible]

instance Paramodulator.S_24.instOfNatNodeOfNatNat : OfNat Node 2

Equations

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

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

@[instance_reducible]

instance Paramodulator.S_24.instOfNatNodeOfNatNat_1 : OfNat Node 3

Equations

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

theorem Paramodulator.S_24.n3_def : 3 = Node.pair 1 1

inductive Paramodulator.S_24.P : Node → Prop

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

@[instance_reducible]

instance Paramodulator.S_24.instOfNatNodeOfNatNat_2 : OfNat Node 4

Equations

• Paramodulator.S_24.instOfNatNodeOfNatNat_2 = { ofNat := Paramodulator.Node.pair 2 0 }

theorem Paramodulator.S_24.n4_def : 4 = Node.pair 2 0

@[instance_reducible]

instance Paramodulator.S_24.instOfNatNodeOfNatNat_3 : OfNat Node 5

Equations

• Paramodulator.S_24.instOfNatNodeOfNatNat_3 = { ofNat := Paramodulator.Node.pair 4 1 }

theorem Paramodulator.S_24.n5_def : 5 = Node.pair 4 1

@[instance_reducible]

instance Paramodulator.S_24.instOfNatNodeOfNatNat_4 : OfNat Node 6

Equations

• Paramodulator.S_24.instOfNatNodeOfNatNat_4 = { ofNat := Paramodulator.Node.pair 1 5 }

theorem Paramodulator.S_24.n6_def : 6 = Node.pair 1 5

@[instance_reducible]

instance Paramodulator.S_24.instOfNatNodeOfNatNat_5 : OfNat Node 7

Equations

• Paramodulator.S_24.instOfNatNodeOfNatNat_5 = { ofNat := Paramodulator.Node.pair 6 4 }

theorem Paramodulator.S_24.n7_def : 7 = Node.pair 6 4

@[instance_reducible]

instance Paramodulator.S_24.instOfNatNodeOfNatNat_6 : OfNat Node 8

Equations

• Paramodulator.S_24.instOfNatNodeOfNatNat_6 = { ofNat := Paramodulator.Node.pair 2 7 }

theorem Paramodulator.S_24.n8_def : 8 = Node.pair 2 7

@[instance_reducible]

instance Paramodulator.S_24.instOfNatNodeOfNatNat_7 : OfNat Node 9

Equations

• Paramodulator.S_24.instOfNatNodeOfNatNat_7 = { ofNat := Paramodulator.Node.pair 3 8 }

theorem Paramodulator.S_24.n9_def : 9 = Node.pair 3 8

inductive Paramodulator.S_24.P' : Node → Prop

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

inductive Paramodulator.S_24.PD : Node → Type

• r0 : PD (Node.pair 3 (Node.pair 2 ((Node.pair 1 ((Node.pair 2 0).pair 1)).pair (Node.pair 2 0))))
• r1 {a : Node} : PD a → PD ((a.pair 0).pair a)
• r2 {a b : Node} : PD (a.pair (Node.pair 1 b)) → PD b
• r3 : PD 0 → PD 2
• r4 {a : Node} : PD a → PD (a.pair 2)
• r5 {a b : Node} : PD (((a.pair (Node.pair 0 a)).pair a).pair b) → PD a → PD 3 → PD a → PD a → PD b
• r6 {a : Node} : PD a → PD 2 → PD (Node.pair 0 a)

theorem Paramodulator.S_24.p_iff_nonempty_pd {a : Node} : P a ↔ Nonempty (PD a)

theorem Paramodulator.S_24.p_9 : P 9

theorem Paramodulator.S_24.not_pd_0_2_3_rl1 {a : Node} (h : PD a) : a ≠ 0 ∧ a ≠ 2 ∧ a ≠ 3 ∧ ∀ ⦃x y : Node⦄, a ≠ x.pair (Node.pair 1 y)

theorem Paramodulator.S_24.not_p_0_2_3_rl1 {a : Node} (h : P a) : a ≠ 0 ∧ a ≠ 2 ∧ a ≠ 3 ∧ ∀ (x y : Node), a ≠ x.pair (Node.pair 1 y)

theorem Paramodulator.S_24.not_p_0 : ¬P 0

theorem Paramodulator.S_24.not_p_2 : ¬P 2

theorem Paramodulator.S_24.not_p_3 : ¬P 3

theorem Paramodulator.S_24.not_p_rl1 {a b : Node} : ¬P (a.pair (Node.pair 1 b))

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