NF weak partition development: NominalWPPReplayChunk017Compact001Part067.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstopfixedhitcontrgrowfixdndv (ph ps ch : SemanticCore.Wff) (x y : SemanticCore.Var) (C : SemanticCore.Class) (k m n : SemanticCore.Var) (F I : SemanticCore.Class) (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_x : x ∉ C.fv) (dv_C_y : y ∉ 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_x : x ∉ F.fv) (dv_F_y : y ∉ F.fv) (dv_I_k : k ∉ I.fv) (dv_I_m : m ∉ I.fv) (dv_I_n : n ∉ I.fv) (_dv_I_p : p ∉ I.fv) (dv_I_x : x ∉ I.fv) (dv_I_y : y ∉ I.fv) (dv_ch_n : n ∉ ch.fv) (_dv_ch_p : p ∉ ch.fv) (dv_ch_x : x ∉ ch.fv) (dv_ch_y : y ∉ ch.fv) (dv_k_m : k ≠ m) (dv_k_n : k ≠ n) (_dv_k_p : k ≠ p) (dv_k_x : k ≠ x) (dv_k_y : k ≠ y) (dv_m_n : m ≠ n) (_dv_m_p : m ≠ p) (dv_m_x : m ≠ x) (_dv_m_y : m ≠ y) (_dv_n_p : n ≠ p) (dv_n_ph : n ∉ ph.fv) (dv_n_ps : n ∉ ps.fv) (dv_n_x : n ≠ x) (dv_n_y : n ≠ y) (_dv_p_ph : p ∉ ph.fv) (_dv_p_ps : p ∉ ps.fv) (_dv_p_x : p ≠ x) (dv_p_y : p ≠ y) (dv_ph_x : x ∉ ph.fv) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_ps_y : y ∉ ps.fv) (dv_x_y : x ≠ y) (hyp_wppstopfixedhitcontrgrowfixdndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCfuns)) (hyp_wppstopfixedhitcontrgrowfixdndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn F) (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopfixedhitcontrgrowfixdndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopfixedhitcontrgrowfixdndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C) Compiler.CompactSourceSyntax.synClec C)) (hyp_wppstopfixedhitcontrgrowfixdndv_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))))) (hyp_wppstopfixedhitcontrgrowfixdndv_6 : 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)))))) (hyp_wppstopfixedhitcontrgrowfixdndv_7 : Nominal.NPrf (SemanticCore.Wff.classMem I (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) (hyp_wppstopfixedhitcontrgrowfixdndv_9 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral y (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv) ((Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv y)))))) (hyp_wppstopfixedhitcontrgrowfixdndv_10 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCwpphit (Compiler.CompactSourceSyntax.synCwppstopstep F C) I C)) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit (Compiler.CompactSourceSyntax.synCwppstopstep F C) I C)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n)))))))) (hyp_wppstopfixedhitcontrgrowfixdndv_11 : Nominal.NPrf (ps.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv 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 I) (Compiler.CompactSourceSyntax.synCtc C))) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) (Compiler.CompactSourceSyntax.synCwpphit (Compiler.CompactSourceSyntax.synCwppstopstep F (Compiler.CompactSourceSyntax.synCtc C)) (Compiler.CompactSourceSyntax.synCtc I) (Compiler.CompactSourceSyntax.synCtc C))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n)))))))) (hyp_wppstopfixedhitcontrgrowfixdndv_12 : Nominal.NPrf (ch.imp (Compiler.CompactSourceSyntax.synWral y (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCwppstopstep F C)) ((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc C) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv y)).imp (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCwppstopstep F C) (SemanticCore.Class.cv y))))))) : Nominal.NPrf ((SemanticCore.Wff.classEq I (Compiler.CompactSourceSyntax.synCtc I)).imp ((Compiler.CompactSourceSyntax.synWa ph (Compiler.CompactSourceSyntax.synWa ps ch)).imp (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synC0c).neg))

Checked nominal proof certificate identified upstream as g_wppstopfixedhitcontrgrowfixdndv.

Equations

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