Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart051.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.withFreshCardinalityVariables (A B : SemanticCore.Class) (n : SemanticCore.Var) (M : SemanticCore.Class) {Result : Sort u} (continuation : (a b m k c x d y e z f w : SemanticCore.Var) → a ∉ A.fv → a ∉ B.fv → a ≠ n → n ≠ a → a ∉ M.fv → b ∉ A.fv → b ∉ B.fv → b ≠ n → n ≠ b → b ∉ M.fv → m ≠ n → n ≠ m → m ∉ M.fv → k ≠ n → n ≠ k → c ≠ n → x ≠ n → d ≠ n → y ≠ n → e ≠ n → n ≠ e → z ≠ n → n ≠ z → f ≠ n → n ≠ f → w ≠ n → n ≠ w → a ≠ b → a ≠ m → m ≠ a → a ≠ k → k ≠ a → c ≠ a → x ≠ a → d ≠ a → y ≠ a → a ≠ e → e ≠ a → z ≠ a → a ≠ f → f ≠ a → w ≠ a → b ≠ m → m ≠ b → b ≠ k → k ≠ b → c ≠ b → x ≠ b → d ≠ b → y ≠ b → ⋯) : Result

Provide the fresh variables used by the finite-cardinality certificate.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.finiteCardinalityInitialCertificates (A B : SemanticCore.Class) (n : SemanticCore.Var) (M : SemanticCore.Class) (a b m k c x d y e z f w : SemanticCore.Var) (fresh_a_ne_n : a ≠ n) (fresh_n_ne_a : n ≠ a) (fresh_a_not_M : a ∉ M.fv) (fresh_b_ne_n : b ≠ n) (fresh_n_ne_b : n ≠ b) (fresh_b_not_M : b ∉ M.fv) (fresh_m_ne_n : m ≠ n) (fresh_n_ne_m : n ≠ m) (fresh_n_ne_k : n ≠ k) (fresh_n_ne_e : n ≠ e) (fresh_n_ne_z : n ≠ z) (fresh_n_ne_f : n ≠ f) (fresh_n_ne_w : n ≠ w) (fresh_a_ne_b : a ≠ b) (fresh_a_ne_m : a ≠ m) (fresh_a_ne_k : a ≠ k) (fresh_c_ne_a : c ≠ a) (fresh_x_ne_a : x ≠ a) (fresh_d_ne_a : d ≠ a) (fresh_y_ne_a : y ≠ a) (fresh_a_ne_e : a ≠ e) (fresh_a_ne_f : a ≠ f) (fresh_b_ne_m : b ≠ m) (fresh_b_ne_k : b ≠ k) (fresh_c_ne_b : c ≠ b) (fresh_x_ne_b : x ≠ b) (fresh_d_ne_b : d ≠ b) (fresh_y_ne_b : y ≠ b) (fresh_b_ne_e : b ≠ e) (fresh_b_ne_f : b ≠ f) (fresh_m_ne_e : m ≠ e) (fresh_m_ne_z : m ≠ z) (fresh_m_ne_f : m ≠ f) (fresh_m_ne_w : m ≠ w) (fresh_c_ne_k : c ≠ k) (fresh_d_ne_k : d ≠ k) (fresh_c_ne_x : c ≠ x) (fresh_c_ne_d : c ≠ d) (fresh_d_ne_c : d ≠ c) (fresh_c_ne_y : c ≠ y) (fresh_y_ne_c : y ≠ c) (fresh_x_ne_d : x ≠ d) (fresh_d_ne_x : d ≠ x) (fresh_x_ne_y : x ≠ y) (fresh_y_ne_x : y ≠ x) (fresh_d_ne_y : d ≠ y) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab m (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv m)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv m))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n))))))) Compiler.CompactSourceSyntax.synCvv) ×' Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synC0c).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv m)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv m))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))) (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) Compiler.CompactSourceSyntax.synC0c) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) Compiler.CompactSourceSyntax.synC0c)).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))))) ×' Nominal.NPrf ((SemanticCore.Wff.objEq m k).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv m)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv m))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))) (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv k))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))))) ×' Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synC1c)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv m)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv m))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))) (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synC1c))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))))) ×' Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv m) M).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv m)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv m))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))) (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) M) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) M)).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))))) ×' n ∉ Compiler.CompactSourceSyntax.synCnnc.fv ×' n ∉ (SemanticCore.Class.cv a).fv ×' n ∉ (SemanticCore.Class.cv b).fv ×' Nominal.NPrf (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) Compiler.CompactSourceSyntax.synC0c) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) Compiler.CompactSourceSyntax.synC0c)).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))) ×' Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf a (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv k))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))))) ×' Nominal.NPrf (Compiler.CompactSourceSyntax.synWnf b (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv k))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))))) ×' d ∉ (SemanticCore.Class.cv k).fv ×' c ∉ (SemanticCore.Class.cv k).fv ×' d ∉ (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)).fv ×' c ∉ (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)).fv ×' y ∉ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv c)).fv ×' y ∉ (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)).fv ×' x ∉ (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)).fv ×' c ∉ (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)).fv ×' x ∉ (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)).fv ×' d ∉ (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)).fv ×' y ∉ (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)).fv ×' Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synC1c))) (Compiler.CompactSourceSyntax.synWrex c (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synWrex d (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv c)) (Compiler.CompactSourceSyntax.synWrex y (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv d)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))))))) ×' a ∉ Compiler.CompactSourceSyntax.synCnnc.fv.erase n ×' b ∉ Compiler.CompactSourceSyntax.synCnnc.fv.erase n ×' Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv e)) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv f)) (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem z e).neg (SemanticCore.Wff.objMem w f).neg))).imp ((SemanticCore.Wff.all a (SemanticCore.Wff.all b ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv b)) (SemanticCore.Class.cv k))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem a n) (SemanticCore.Wff.objMem b n)))))).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem e n) (SemanticCore.Wff.objMem f n))))) ×' m ∉ Compiler.CompactSourceSyntax.synC1c.fv ×' m ∉ Compiler.CompactSourceSyntax.synCnnc.fv ×' m ∉ (SemanticCore.Class.cv e).fv ×' m ∉ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z)).fv ×' m ∉ (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))).fv ×' m ∉ (SemanticCore.Class.cv f).fv ×' m ∉ (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv w)).fv ×' m ∉ (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv w))).fv ×' Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv e)) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv f)) (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem z e).neg (SemanticCore.Wff.objMem w f).neg))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synCnnc)).imp ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem e n) (SemanticCore.Wff.objMem f n)).imp (Compiler.CompactSourceSyntax.synWrex m Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (SemanticCore.Class.cv m)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv w))) (SemanticCore.Class.cv m)))))) ×' n ∉ (Compiler.CompactSourceSyntax.synWrex m Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z))) (SemanticCore.Class.cv m)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv w))) (SemanticCore.Class.cv m)))).fv ×' n ∉ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv e)) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv f)) (SemanticCore.Class.cv k))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem z e).neg (SemanticCore.Wff.objMem w f).neg))).fv

Construct the initial finite-cardinality certificates and their freshness evidence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNcfinlower (A B : SemanticCore.Class) (n : SemanticCore.Var) (M : SemanticCore.Class) (dv_A_n : n ∉ A.fv) (dv_B_n : n ∉ B.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 A) M) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 B) M)).imp (Compiler.CompactSourceSyntax.synWrex n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A (SemanticCore.Class.cv n)) (SemanticCore.Wff.classMem B (SemanticCore.Class.cv n)))))

Checked nominal proof certificate identified upstream as g_ncfinlower.

Certificates from NominalWPPReplayChunk009StructuralPart052.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnpw1ex (n : SemanticCore.Var) (M : SemanticCore.Class) (a : SemanticCore.Var) (dv_M_a : a ∉ M.fv) (dv_M_n : n ∉ M.fv) (dv_a_n : a ≠ n) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWne M Compiler.CompactSourceSyntax.synC0)).imp (Compiler.CompactSourceSyntax.synWreu n Compiler.CompactSourceSyntax.synCnnc (Compiler.CompactSourceSyntax.synWrex a M (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv a)) (SemanticCore.Class.cv n)))))

Checked nominal proof certificate identified upstream as g_nnpw1ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTfinex (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtfin A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_tfinex.

Equations

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