Documentation

Projects.Paramodulator.Systems.S_32

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat :

Equations

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

theorem Paramodulator.S_32.n2_def :

2 = Node.pair 1 0

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat_1 :

Equations

Paramodulator.S_32.instOfNatNodeOfNatNat_1 = { ofNat := Paramodulator.Node.pair 0 1 }

theorem Paramodulator.S_32.n3_def :

3 = Node.pair 0 1

inductive Paramodulator.S_32.P :

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

Instances For

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat_2 :

Equations

Paramodulator.S_32.instOfNatNodeOfNatNat_2 = { ofNat := Paramodulator.Node.pair 1 1 }

theorem Paramodulator.S_32.n4_def :

4 = Node.pair 1 1

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat_3 :

Equations

Paramodulator.S_32.instOfNatNodeOfNatNat_3 = { ofNat := Paramodulator.Node.pair 0 4 }

theorem Paramodulator.S_32.n5_def :

5 = Node.pair 0 4

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat_4 :

Equations

Paramodulator.S_32.instOfNatNodeOfNatNat_4 = { ofNat := Paramodulator.Node.pair 5 0 }

theorem Paramodulator.S_32.n6_def :

6 = Node.pair 5 0

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat_5 :

Equations

Paramodulator.S_32.instOfNatNodeOfNatNat_5 = { ofNat := Paramodulator.Node.pair 6 1 }

theorem Paramodulator.S_32.n7_def :

7 = Node.pair 6 1

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat_6 :

Equations

Paramodulator.S_32.instOfNatNodeOfNatNat_6 = { ofNat := Paramodulator.Node.pair 7 1 }

theorem Paramodulator.S_32.n8_def :

8 = Node.pair 7 1

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat_7 :

Equations

Paramodulator.S_32.instOfNatNodeOfNatNat_7 = { ofNat := Paramodulator.Node.pair 0 8 }

theorem Paramodulator.S_32.n9_def :

9 = Node.pair 0 8

@[instance_reducible]

instance Paramodulator.S_32.instOfNatNodeOfNatNat_8 :

Equations

Paramodulator.S_32.instOfNatNodeOfNatNat_8 = { ofNat := Paramodulator.Node.pair 0 9 }

theorem Paramodulator.S_32.n10_def :

10 = Node.pair 0 9

theorem Paramodulator.S_32.p_eq :

P = fun (x : Node) => x ∈ {0, 1, 8, 9, 10}