Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part019.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFpivelfdif (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_d : d ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_d : d ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_R_d : d ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_d_x : d ≠ x) (dv_d_y : d ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfpiv R A (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfdif R A B)))

Checked nominal proof certificate identified upstream as g_fpivelfdif.

Equations

• One or more equations did not get rendered due to their size.

Certificates from NominalWPPReplayChunk014Compact001Part020.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdrowsep (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_d : d ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_d : d ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_R_d : d ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_d_x : d ≠ x) (dv_d_y : d ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfpiv R A (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).imp (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_fdrowsep.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSep2ex2 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCsep2 (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_sep2ex2.

Equations

• One or more equations did not get rendered due to their size.

Certificates from NominalWPPReplayChunk014Compact001Part021.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFpivex (x y : SemanticCore.Var) (A R : SemanticCore.Class) (b d : SemanticCore.Var) (dv_A_R : Disjoint A.fv R.fv) (dv_A_b : b ∉ A.fv) (dv_A_d : d ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (_dv_R_b : b ∉ R.fv) (dv_R_d : d ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_b_d : b ≠ d) (dv_b_x : b ≠ x) (dv_b_y : b ≠ y) (dv_d_x : d ≠ x) (dv_d_y : d ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWrex b A (SemanticCore.Wff.classMem (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCsep2 (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))).imp (Compiler.CompactSourceSyntax.synWrex d A (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfpiv R A (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))

Checked nominal proof certificate identified upstream as g_fpivex.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdrowdiff (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_R : Disjoint B.fv R.fv) (_dv_B_b : b ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_R_b : b ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_b_x : b ≠ x) (dv_b_y : b ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (Compiler.CompactSourceSyntax.synWrex b A (SemanticCore.Wff.classMem (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCsep2 (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))).imp (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as g_fdrowdiff.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdroweqnosep (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_b : b ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_R_b : b ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_b_x : b ≠ x) (dv_b_y : b ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv y)))).imp (Compiler.CompactSourceSyntax.synWrex b A (SemanticCore.Wff.classMem (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCsep2 (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).neg)

Checked nominal proof certificate identified upstream as g_fdroweqnosep.

Equations

• One or more equations did not get rendered due to their size.

Certificates from NominalWPPReplayChunk014Compact001Part022.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdroweqmem (x y : SemanticCore.Var) (A B C R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (_dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (_dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (_dv_C_R : Disjoint C.fv R.fv) (_dv_C_x : x ∉ C.fv) (_dv_C_y : y ∉ C.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) B)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv y)))) (SemanticCore.Wff.classMem C A)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) C)))

Checked nominal proof certificate identified upstream as g_fdroweqmem.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdrowrelex2 (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdrowrelex2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdrowrelex2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdrowrelex2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdrowrel R A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fdrowrelex2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfdrowfibg (A B C D R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (_dv_A_D : Disjoint A.fv D.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (_dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (_dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (_dv_D_R : Disjoint D.fv R.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfdrowfib R A B C)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCsn D) C) (Compiler.CompactSourceSyntax.synCfdrowrel R A B))))

Checked nominal proof certificate identified upstream as g_elfdrowfibg.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdrowfibeq4 (A B C D R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_D : Disjoint A.fv D.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (_dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_D_R : Disjoint D.fv R.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq C D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdrowfib R A B C) (Compiler.CompactSourceSyntax.synCfdrowfib R A B D)))

Checked nominal proof certificate identified upstream as g_fdrowfibeq4.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdrowfibsn2 (A B C R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_R : Disjoint C.fv R.fv) (hyp_fdrowfibsn2_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdrowfib R A B (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synCfdrow R A B C))

Checked nominal proof certificate identified upstream as g_fdrowfibsn2.

Equations

• One or more equations did not get rendered due to their size.