Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk017Compact001Part062.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gHwcardslecconnexndv (K L : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem K (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classMem L (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))).imp (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWbr K Compiler.CompactSourceSyntax.synClec L) (Compiler.CompactSourceSyntax.synWbr L Compiler.CompactSourceSyntax.synClec K)))

Checked nominal proof certificate identified upstream as g_hwcardslecconnexndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpporbithwcldmndv (F I : SemanticCore.Class) (q : SemanticCore.Var) (_dv_F_q : q ∉ F.fv) (_dv_I_q : q ∉ I.fv) (hyp_wpporbithwcldmndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wpporbithwcldmndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpporbithwcldmndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wpporbithwcldmndv_4 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfrec F I) (SemanticCore.Class.cv q)) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)))

Checked nominal proof certificate identified upstream as g_wpporbithwcldmndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part063.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppgammaprefixeqhwselfmapndv (y : SemanticCore.Var) (F G L : SemanticCore.Class) (dv_F_y : y ∉ F.fv) (dv_G_y : y ∉ G.fv) (dv_L_y : y ∉ L.fv) (hyp_wppgammaprefixeqhwselfmapndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppgammaprefixeqhwselfmapndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppgammaprefixeqhwselfmapndv_3 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppgammaprefixeqhwselfmapndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppgammaprefixeqhwselfmapndv_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppgammaprefixeqhwselfmapndv_6 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm G) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppgammaprefixeqhwselfmapndv_7 : Nominal.NPrf (SemanticCore.Wff.classMem L (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppgammaprefixeqhwselfmapndv_8 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral y (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synClec L).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv F (SemanticCore.Class.cv y)) (Compiler.CompactSourceSyntax.synCfv G (SemanticCore.Class.cv y)))))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwppgamma F L) (Compiler.CompactSourceSyntax.synCwppgamma G L))

Checked nominal proof certificate identified upstream as g_wppgammaprefixeqhwselfmapndv.

Equations

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

Certificates from NominalWPPReplayChunk017Compact001Part064.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopgammaprefixeqndv (C F : SemanticCore.Class) (p : SemanticCore.Var) (dv_C_p : p ∉ C.fv) (dv_F_p : p ∉ F.fv) (hyp_wppstopgammaprefixeqndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopgammaprefixeqndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopgammaprefixeqndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopgammaprefixeqndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C) Compiler.CompactSourceSyntax.synClec C)) (hyp_wppstopgammaprefixeqndv_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm F))))) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F (Compiler.CompactSourceSyntax.synCtc C)) (Compiler.CompactSourceSyntax.synCtc C)) (Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F C) (Compiler.CompactSourceSyntax.synCtc C)))

Checked nominal proof certificate identified upstream as g_wppstopgammaprefixeqndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWpphitstartcongrndv (C F I J : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq I J).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCwpphit F I C) (Compiler.CompactSourceSyntax.synCwpphit F J C)))

Checked nominal proof certificate identified upstream as g_wpphitstartcongrndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcrossgammaleasthitpairhwndv (C : SemanticCore.Class) (k m n : SemanticCore.Var) (F G : SemanticCore.Class) (q p : SemanticCore.Var) (dv_C_k : k ∉ C.fv) (dv_C_m : m ∉ C.fv) (dv_C_n : n ∉ C.fv) (dv_C_p : p ∉ C.fv) (dv_C_q : q ∉ C.fv) (_dv_F_k : k ∉ F.fv) (dv_F_m : m ∉ F.fv) (dv_F_n : n ∉ F.fv) (dv_F_p : p ∉ F.fv) (_dv_F_q : q ∉ F.fv) (dv_G_k : k ∉ G.fv) (_dv_G_m : m ∉ G.fv) (_dv_G_n : n ∉ G.fv) (dv_G_p : p ∉ G.fv) (dv_G_q : q ∉ G.fv) (_dv_k_m : k ≠ m) (_dv_k_n : k ≠ n) (_dv_k_p : k ≠ p) (dv_k_q : k ≠ q) (dv_m_n : m ≠ n) (_dv_m_p : m ≠ p) (_dv_m_q : m ≠ q) (_dv_n_p : n ≠ p) (_dv_n_q : n ≠ q) (_dv_p_q : p ≠ q) (hyp_wppcrossgammaleasthitpairhwndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppcrossgammaleasthitpairhwndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synCdm F))) (hyp_wppcrossgammaleasthitpairhwndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec C).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm F))))) (hyp_wppcrossgammaleasthitpairhwndv_4 : Nominal.NPrf (SemanticCore.Wff.classMem G Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppcrossgammaleasthitpairhwndv_5 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn G) (Compiler.CompactSourceSyntax.synCdm G))) (hyp_wppcrossgammaleasthitpairhwndv_6 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral p (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv p) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc C)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCdm G))))) (hyp_wppcrossgammaleasthitpairhwndv_7 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppcrossgammaleasthitpairhwndv_8 : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCwppgamma F C)) (Compiler.CompactSourceSyntax.synCwppgamma G (Compiler.CompactSourceSyntax.synCtc C)))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex m Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCwpphit F (Compiler.CompactSourceSyntax.synCwppgamma F C) C)) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit F (Compiler.CompactSourceSyntax.synCwppgamma F C) C)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n)))))) (Compiler.CompactSourceSyntax.synWrex k Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwpphit G (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCwppgamma F C)) (Compiler.CompactSourceSyntax.synCtc C))) (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCwpphit G (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCwppgamma F C)) (Compiler.CompactSourceSyntax.synCtc C))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv q)))))))

Checked nominal proof certificate identified upstream as g_wppcrossgammaleasthitpairhwndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopgammaleasthitpairndv (x : SemanticCore.Var) (C : SemanticCore.Class) (k m n : SemanticCore.Var) (F : SemanticCore.Class) (q : SemanticCore.Var) (dv_C_k : k ∉ C.fv) (dv_C_m : m ∉ C.fv) (dv_C_n : n ∉ C.fv) (dv_C_q : q ∉ C.fv) (dv_C_x : x ∉ C.fv) (dv_F_k : k ∉ F.fv) (dv_F_m : m ∉ F.fv) (dv_F_n : n ∉ F.fv) (dv_F_q : q ∉ F.fv) (dv_F_x : x ∉ F.fv) (dv_k_m : k ≠ m) (dv_k_n : k ≠ n) (dv_k_q : k ≠ q) (_dv_k_x : k ≠ x) (dv_m_n : m ≠ n) (dv_m_q : m ≠ q) (_dv_m_x : m ≠ x) (dv_n_q : n ≠ q) (_dv_n_x : n ≠ x) (_dv_q_x : q ≠ x) (hyp_wppstopgammaleasthitpairndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopgammaleasthitpairndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopgammaleasthitpairndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopgammaleasthitpairndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral x (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep F C)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F (Compiler.CompactSourceSyntax.synCtc C)) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv x)))))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWrex m Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCwpphit (Compiler.CompactSourceSyntax.synCwppstopstep F C) (Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F C) C) C)) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit (Compiler.CompactSourceSyntax.synCwppstopstep F C) (Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F C) C) C)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n)))))) (Compiler.CompactSourceSyntax.synWrex k Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCwpphit (Compiler.CompactSourceSyntax.synCwppstopstep F (Compiler.CompactSourceSyntax.synCtc C)) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F C) C)) (Compiler.CompactSourceSyntax.synCtc C))) (Compiler.CompactSourceSyntax.synWral q Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv q) (Compiler.CompactSourceSyntax.synCwpphit (Compiler.CompactSourceSyntax.synCwppstopstep F (Compiler.CompactSourceSyntax.synCtc C)) (Compiler.CompactSourceSyntax.synCtc (Compiler.CompactSourceSyntax.synCwppgamma (Compiler.CompactSourceSyntax.synCwppstopstep F C) C)) (Compiler.CompactSourceSyntax.synCtc C))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv q)))))))

Checked nominal proof certificate identified upstream as g_wppstopgammaleasthitpairndv.

Equations

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