Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part030.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandstrictsliceleastdndvv (C D R : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) (q : SemanticCore.Var) (dv_C_k : k ∉ C.fv) (dv_C_m : m ∉ C.fv) (dv_C_q : q ∉ C.fv) (dv_D_k : k ∉ D.fv) (dv_D_m : m ∉ D.fv) (dv_D_q : q ∉ D.fv) (dv_F_k : k ∉ F.fv) (dv_F_m : m ∉ F.fv) (dv_F_q : q ∉ F.fv) (dv_R_k : k ∉ R.fv) (dv_R_m : m ∉ R.fv) (dv_R_q : q ∉ R.fv) (dv_k_m : k ≠ m) (dv_k_q : k ≠ q) (_dv_m_q : m ≠ q) (hyp_wppcandstrictsliceleastdndvv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wppcandstrictsliceleastdndvv_2 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wppcandstrictsliceleastdndvv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWrex m (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))))

Checked nominal proof certificate identified upstream as g_wppcandstrictsliceleastdndvv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandstrictsliceleastextenddv (z : SemanticCore.Var) (C : SemanticCore.Class) (k m : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_k : k ∉ C.fv) (_dv_C_m : m ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_F_k : k ∉ F.fv) (_dv_F_m : m ∉ F.fv) (dv_F_z : z ∉ F.fv) (dv_k_m : k ≠ m) (dv_k_z : k ≠ z) (dv_m_z : m ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C)))) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCwppcand F C)) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv z)))))

Checked nominal proof certificate identified upstream as g_wppcandstrictsliceleastextenddv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part031.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisobranchwwknfdv (x y u : SemanticCore.Var) (D R S : SemanticCore.Class) (h : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_h : h ∉ D.fv) (_dv_D_u : u ∉ D.fv) (_dv_D_x : x ∉ D.fv) (_dv_D_y : y ∉ D.fv) (dv_E_h : h ∉ E.fv) (_dv_E_u : u ∉ E.fv) (_dv_E_x : x ∉ E.fv) (_dv_E_y : y ∉ E.fv) (dv_R_h : h ∉ R.fv) (_dv_R_u : u ∉ R.fv) (_dv_R_x : x ∉ R.fv) (_dv_R_y : y ∉ R.fv) (dv_S_h : h ∉ S.fv) (_dv_S_u : u ∉ S.fv) (_dv_S_x : x ∉ S.fv) (_dv_S_y : y ∉ S.fv) (dv_h_u : h ≠ u) (_dv_h_x : h ≠ x) (dv_h_y : h ≠ y) (_dv_u_x : u ≠ x) (_dv_u_y : u ≠ y) (_dv_x_y : x ≠ y) (_hyp_wecutisobranchknterminalfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (_hyp_wecutisobranchknterminalfdv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) (hyp_wecutisobranchknterminalfdv_3 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).neg.imp ((Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv u)))) R S (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) D) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))) E)).imp (Compiler.CompactSourceSyntax.synW3o (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R S D E)) (Compiler.CompactSourceSyntax.synWrex x E (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) D (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))) (Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) S (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) E (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))))))))

Checked nominal proof certificate identified upstream as g_wecutisobranchwwknfdv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part032.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisobranchwcknfdv (x y v u : SemanticCore.Var) (D R S : SemanticCore.Class) (h : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_h : h ∉ D.fv) (_dv_D_u : u ∉ D.fv) (_dv_D_v : v ∉ D.fv) (dv_D_x : x ∉ D.fv) (_dv_D_y : y ∉ D.fv) (dv_E_h : h ∉ E.fv) (_dv_E_u : u ∉ E.fv) (_dv_E_v : v ∉ E.fv) (dv_E_x : x ∉ E.fv) (_dv_E_y : y ∉ E.fv) (dv_R_h : h ∉ R.fv) (_dv_R_u : u ∉ R.fv) (_dv_R_v : v ∉ R.fv) (dv_R_x : x ∉ R.fv) (_dv_R_y : y ∉ R.fv) (dv_S_h : h ∉ S.fv) (_dv_S_u : u ∉ S.fv) (_dv_S_v : v ∉ S.fv) (dv_S_x : x ∉ S.fv) (_dv_S_y : y ∉ S.fv) (dv_h_u : h ≠ u) (dv_h_v : h ≠ v) (dv_h_x : h ≠ x) (dv_h_y : h ≠ y) (_dv_u_v : u ≠ v) (_dv_u_x : u ≠ x) (_dv_u_y : u ≠ y) (dv_v_x : v ≠ x) (_dv_v_y : v ≠ y) (_dv_x_y : x ≠ y) (_hyp_wecutisobranchknterminalfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (_hyp_wecutisobranchknterminalfdv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) (hyp_wecutisobranchknterminalfdv_3 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).neg.imp ((Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (SemanticCore.Class.cv u)))) R S (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) E)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv v)))))).imp (Compiler.CompactSourceSyntax.synW3o (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R S D E)) (Compiler.CompactSourceSyntax.synWrex x E (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) D (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))) (Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) S (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) E (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))))))))

Checked nominal proof certificate identified upstream as g_wecutisobranchwcknfdv.

Equations

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