NF weak partition development: NFStandard.HailperinCylinder.

The hard-direction compiler uses one integer type ceiling (cap) for a whole formula. Every coordinate is first raised to that ceiling by iterated singletons. The resulting homogeneous coordinates are then encoded by Hailperin's type-correct tuple convention: a head is padded by two singleton levels for every ordered-pair layer below it.

Iterated singleton raising

noncomputable def NFChoice.Foundation.NFStandard.raise {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : ℕ → S.carrier → S.carrier

Raise a value by m singleton levels.

Equations

• NFChoice.Foundation.NFStandard.raise hH 0 x✝ = x✝
• NFChoice.Foundation.NFStandard.raise hH m.succ x✝ = NFChoice.Foundation.NFStandard.singleton hH (NFChoice.Foundation.NFStandard.raise hH m x✝)

@[simp]

theorem NFChoice.Foundation.NFStandard.raise_zero {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (a : S.carrier) : raise hH 0 a = a

@[simp]

theorem NFChoice.Foundation.NFStandard.raise_succ {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (a : S.carrier) : raise hH (m + 1) a = singleton hH (raise hH m a)

theorem NFChoice.Foundation.NFStandard.mem_raise_succ {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (a z : S.carrier) : SemanticCore.Mem S z (raise hH (m + 1) a) ↔ z = raise hH m a

theorem NFChoice.Foundation.NFStandard.singleton_injective {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : Function.Injective (singleton hH)

theorem NFChoice.Foundation.NFStandard.raise_injective {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) : Function.Injective (raise hH m)

@[simp]

theorem NFChoice.Foundation.NFStandard.raise_eq_raise_iff {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (a b : S.carrier) : raise hH m a = raise hH m b ↔ a = b

theorem NFChoice.Foundation.NFStandard.raise_add {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m k : ℕ) (a : S.carrier) : raise hH (m + k) a = raise hH m (raise hH k a)

Kuratowski-pair injectivity

theorem NFChoice.Foundation.NFStandard.unorderedPair_eq_iff {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (a b c d : S.carrier) : unorderedPair hH a b = unorderedPair hH c d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

theorem NFChoice.Foundation.NFStandard.singleton_eq_unorderedPair_iff {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (a b c : S.carrier) : singleton hH a = unorderedPair hH b c ↔ b = a ∧ c = a

theorem NFChoice.Foundation.NFStandard.kPair_injective {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {a b c d : S.carrier} (h : kPair hH a b = kPair hH c d) : a = c ∧ b = d

Homogeneous tuple codes

noncomputable def NFChoice.Foundation.NFStandard.htuple {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} : DVec S.carrier n → S.carrier

Encode a homogeneous tuple. At arity one the code is its sole coordinate. At each further layer, the head receives exactly the singleton padding needed to have the same type as the already encoded tail.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Foundation.NFStandard.htuple hH NFChoice.DVec.nil = NFChoice.Foundation.NFStandard.oneC hH
• NFChoice.Foundation.NFStandard.htuple hH (NFChoice.DVec.cons a NFChoice.DVec.nil) = a

@[simp]

theorem NFChoice.Foundation.NFStandard.htuple_nil {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : htuple hH DVec.nil = oneC hH

@[simp]

theorem NFChoice.Foundation.NFStandard.htuple_one {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (a : S.carrier) : htuple hH (DVec.cons a DVec.nil) = a

theorem NFChoice.Foundation.NFStandard.htuple_two {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (a b : S.carrier) : htuple hH (DVec.cons a (DVec.cons b DVec.nil)) = kPair hH a b

@[simp]

theorem NFChoice.Foundation.NFStandard.htuple_succ_succ {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (a : S.carrier) (xs : DVec S.carrier (n + 1)) : htuple hH (DVec.cons a xs) = kPair hH (raise hH (2 * n) a) (htuple hH xs)

theorem NFChoice.Foundation.NFStandard.htuple_injective {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (n : ℕ) : Function.Injective (htuple hH)

@[simp]

theorem NFChoice.Foundation.NFStandard.htuple_eq_iff {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (xs ys : DVec S.carrier n) : htuple hH xs = htuple hH ys ↔ xs = ys

theorem NFChoice.Foundation.NFStandard.lookup_eq_of_htuple_eq {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} {xs ys : DVec S.carrier n} (h : htuple hH xs = htuple hH ys) (i : Fin n) : SemanticCore.Lowering.lookup xs i = SemanticCore.Lowering.lookup ys i

Fixed-cap normalization

def NFChoice.Foundation.NFStandard.capOffset (cap k : ℤ) : ℕ

Singleton exponent which raises type k to the common cap.

Equations

• NFChoice.Foundation.NFStandard.capOffset cap k = (cap - k).toNat

theorem NFChoice.Foundation.NFStandard.capOffset_cast {cap k : ℤ} (h : k ≤ cap) : ↑(capOffset cap k) = cap - k

noncomputable def NFChoice.Foundation.NFStandard.normalizeVec {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} : (Fin n → ℕ) → DVec S.carrier n → DVec S.carrier n

Apply a coordinate-dependent singleton exponent to a dependent vector.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Foundation.NFStandard.normalizeVec hH x_3 NFChoice.DVec.nil = NFChoice.DVec.nil

@[simp]

theorem NFChoice.Foundation.NFStandard.normalizeVec_nil {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (e : Fin 0 → ℕ) : normalizeVec hH e DVec.nil = DVec.nil

@[simp]

theorem NFChoice.Foundation.NFStandard.normalizeVec_cons {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (e : Fin (n + 1) → ℕ) (a : S.carrier) (xs : DVec S.carrier n) : normalizeVec hH e (DVec.cons a xs) = DVec.cons (raise hH (e 0) a) (normalizeVec hH (fun (i : Fin n) => e i.succ) xs)

@[simp]

theorem NFChoice.Foundation.NFStandard.lookup_normalizeVec {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (e : Fin n → ℕ) (xs : DVec S.carrier n) (i : Fin n) : SemanticCore.Lowering.lookup (normalizeVec hH e xs) i = raise hH (e i) (SemanticCore.Lowering.lookup xs i)

theorem NFChoice.Foundation.NFStandard.normalizeVec_injective {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (e : Fin n → ℕ) : Function.Injective (normalizeVec hH e)

noncomputable def NFChoice.Foundation.NFStandard.valuationCode {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (xs : DVec S.carrier n) : S.carrier

Normalize every coordinate to cap, then encode the homogeneous tuple.

Equations

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

theorem NFChoice.Foundation.NFStandard.raised_coordinate_eq_of_valuationCode_eq {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) {xs ys : DVec S.carrier n} (h : valuationCode hH cap ty xs = valuationCode hH cap ty ys) (i : Fin n) : raise hH (capOffset cap (ty i)) (SemanticCore.Lowering.lookup xs i) = raise hH (capOffset cap (ty i)) (SemanticCore.Lowering.lookup ys i)

theorem NFChoice.Foundation.NFStandard.valuationCode_coordinate {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) {xs ys : DVec S.carrier n} (h : valuationCode hH cap ty xs = valuationCode hH cap ty ys) (i : Fin n) : SemanticCore.Lowering.lookup xs i = SemanticCore.Lowering.lookup ys i

theorem NFChoice.Foundation.NFStandard.valuationCode_injective {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) : Function.Injective (valuationCode hH cap ty)

Boolean relation objects

noncomputable def NFChoice.Foundation.NFStandard.universalObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : S.carrier

A universal set, built as the NAND of a set and its complement.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_universalObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (z : S.carrier) : SemanticCore.Mem S z (universalObj hH)

noncomputable def NFChoice.Foundation.NFStandard.emptyObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : S.carrier

The empty set, derived as the complement of the universal set.

Equations

• NFChoice.Foundation.NFStandard.emptyObj hH = NFChoice.Foundation.NFStandard.complement hH (NFChoice.Foundation.NFStandard.universalObj hH)

@[simp]

theorem NFChoice.Foundation.NFStandard.not_mem_emptyObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (z : S.carrier) : ¬SemanticCore.Mem S z (emptyObj hH)

noncomputable def NFChoice.Foundation.NFStandard.interObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B : S.carrier) : S.carrier

Intersection, derived by complementing NAND.

Equations

• NFChoice.Foundation.NFStandard.interObj hH A B = NFChoice.Foundation.NFStandard.complement hH (NFChoice.Foundation.NFStandard.nin hH A B)

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_interObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B z : S.carrier) : SemanticCore.Mem S z (interObj hH A B) ↔ SemanticCore.Mem S z A ∧ SemanticCore.Mem S z B

Iteration of primitive relation transformers

noncomputable def NFChoice.Foundation.NFStandard.siIter {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : ℕ → S.carrier → S.carrier

Iterate Hailperin's singleton-image transformer.

Equations

• NFChoice.Foundation.NFStandard.siIter hH 0 x✝ = x✝
• NFChoice.Foundation.NFStandard.siIter hH m.succ x✝ = NFChoice.Foundation.NFStandard.si hH (NFChoice.Foundation.NFStandard.siIter hH m x✝)

@[simp]

theorem NFChoice.Foundation.NFStandard.siIter_zero {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A : S.carrier) : siIter hH 0 A = A

@[simp]

theorem NFChoice.Foundation.NFStandard.siIter_succ {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A : S.carrier) : siIter hH (m + 1) A = si hH (siIter hH m A)

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_siIter {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A z w : S.carrier) : SemanticCore.Mem S (kPair hH (raise hH m z) (raise hH m w)) (siIter hH m A) ↔ SemanticCore.Mem S (kPair hH z w) A

noncomputable def NFChoice.Foundation.NFStandard.identityRel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : S.carrier

Identity relation, as mutual inclusion.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_identityRel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (a b : S.carrier) : SemanticCore.Mem S (kPair hH a b) (identityRel hH) ↔ a = b

theorem NFChoice.Foundation.NFStandard.mem_sset_singleton {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (a b : S.carrier) : SemanticCore.Mem S (kPair hH (singleton hH a) b) (sset hH) ↔ SemanticCore.Mem S a b

Inclusion of a singleton is ordinary membership.

theorem NFChoice.Foundation.NFStandard.mem_raisedIdentity {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (a b : S.carrier) : SemanticCore.Mem S (kPair hH (raise hH m a) (raise hH m b)) (siIter hH m (identityRel hH)) ↔ a = b

Equality relation after raising both inputs to the cap.

theorem NFChoice.Foundation.NFStandard.mem_raisedMembership {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (a b : S.carrier) : SemanticCore.Mem S (kPair hH (raise hH (m + 1) a) (raise hH m b)) (siIter hH m (sset hH)) ↔ SemanticCore.Mem S a b

Membership relation after normalizing source and target to one cap.

Kuratowski image and composition

The apparently stronger image operation is already derivable from the primitive Hailperin operators. This is the semantic form of dfimak2 in nf.mm. Isolating it here makes the later coordinate selectors independent of the generated Metamath replay.

theorem NFChoice.Foundation.NFStandard.mem_xp_kPair {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (B a b : S.carrier) : SemanticCore.Mem S (kPair hH a b) (xp hH B) ↔ SemanticCore.Mem S b B

Membership in the primitive V × B constructor on a genuine pair.

theorem NFChoice.Foundation.NFStandard.mem_cnv_xp_kPair {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (B a b : S.carrier) : SemanticCore.Mem S (kPair hH a b) (cnv hH (xp hH B)) ↔ SemanticCore.Mem S a B

Membership in B × V, obtained by conversing V × B.

theorem NFChoice.Foundation.NFStandard.mem_oneC_iff_eq_singleton {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (w : S.carrier) : SemanticCore.Mem S w (oneC hH) ↔ ∃ (y : S.carrier), w = singleton hH y

The chosen 1c consists exactly of the selected singleton objects.

theorem NFChoice.Foundation.NFStandard.mem_oneC_singleton {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (y : S.carrier) : SemanticCore.Mem S (singleton hH y) (oneC hH)

noncomputable def NFChoice.Foundation.NFStandard.imageKernel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B : S.carrier) : S.carrier

The relation used under P6 in the standard construction of image.

Equations

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

theorem NFChoice.Foundation.NFStandard.mem_imageKernel_all {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B z : S.carrier) : (∀ (w : S.carrier), SemanticCore.Mem S (kPair hH w (singleton hH z)) (imageKernel hH A B)) ↔ ∀ (y : S.carrier), ¬(SemanticCore.Mem S y B ∧ SemanticCore.Mem S (kPair hH y z) A)

noncomputable def NFChoice.Foundation.NFStandard.imageObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B : S.carrier) : S.carrier

Image of a set under a Kuratowski relation.

Equations

• NFChoice.Foundation.NFStandard.imageObj hH A B = NFChoice.Foundation.NFStandard.complement hH (NFChoice.Foundation.NFStandard.typeLower hH (NFChoice.Foundation.NFStandard.imageKernel hH A B))

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_imageObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B z : S.carrier) : SemanticCore.Mem S z (imageObj hH A B) ↔ ∃ (y : S.carrier), SemanticCore.Mem S y B ∧ SemanticCore.Mem S (kPair hH y z) A

A raised image is needed because Ins2 and Ins3 deliberately mark their inserted coordinate by two singleton levels. The following small library constructs exact sets of iterated-singleton values, so the image quantifier cannot see any unconstrained noncanonical inputs.

noncomputable def NFChoice.Foundation.NFStandard.powerObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A : S.carrier) : S.carrier

The power set of A, built as an image of the converse subset relation.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_powerObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A z : S.carrier) : SemanticCore.Mem S z (powerObj hH A) ↔ ∀ (w : S.carrier), SemanticCore.Mem S w z → SemanticCore.Mem S w A

noncomputable def NFChoice.Foundation.NFStandard.unitPowerObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A : S.carrier) : S.carrier

Singleton subsets of A, i.e. the direct singleton image of A.

Equations

• NFChoice.Foundation.NFStandard.unitPowerObj hH A = NFChoice.Foundation.NFStandard.interObj hH (NFChoice.Foundation.NFStandard.oneC hH) (NFChoice.Foundation.NFStandard.powerObj hH A)

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_unitPowerObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A z : S.carrier) : SemanticCore.Mem S z (unitPowerObj hH A) ↔ ∃ (x : S.carrier), SemanticCore.Mem S x A ∧ z = singleton hH x

noncomputable def NFChoice.Foundation.NFStandard.raiseImage {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : ℕ → S.carrier → S.carrier

Direct image under m iterations of singleton.

Equations

• NFChoice.Foundation.NFStandard.raiseImage hH 0 x✝ = x✝
• NFChoice.Foundation.NFStandard.raiseImage hH m.succ x✝ = NFChoice.Foundation.NFStandard.unitPowerObj hH (NFChoice.Foundation.NFStandard.raiseImage hH m x✝)

@[simp]

theorem NFChoice.Foundation.NFStandard.raiseImage_zero {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A : S.carrier) : raiseImage hH 0 A = A

@[simp]

theorem NFChoice.Foundation.NFStandard.raiseImage_succ {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A : S.carrier) : raiseImage hH (m + 1) A = unitPowerObj hH (raiseImage hH m A)

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_raiseImage {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A z : S.carrier) : SemanticCore.Mem S z (raiseImage hH m A) ↔ ∃ (x : S.carrier), SemanticCore.Mem S x A ∧ z = raise hH m x

theorem NFChoice.Foundation.NFStandard.mem_raiseImage_exact {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A x : S.carrier) : SemanticCore.Mem S (raise hH m x) (raiseImage hH m A) ↔ SemanticCore.Mem S x A

noncomputable def NFChoice.Foundation.NFStandard.raisedUniversal {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) : S.carrier

All values at singleton level m.

Equations

• NFChoice.Foundation.NFStandard.raisedUniversal hH m = NFChoice.Foundation.NFStandard.raiseImage hH m (NFChoice.Foundation.NFStandard.universalObj hH)

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_raisedUniversal {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (z : S.carrier) : SemanticCore.Mem S z (raisedUniversal hH m) ↔ ∃ (x : S.carrier), z = raise hH m x

noncomputable def NFChoice.Foundation.NFStandard.raisedImageKernel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A B : S.carrier) : S.carrier

dfimak2 with the quantified first coordinate raised by m levels.

Equations

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

theorem NFChoice.Foundation.NFStandard.mem_raisedImageKernel_all {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A B z : S.carrier) : (∀ (w : S.carrier), SemanticCore.Mem S (kPair hH w (singleton hH z)) (raisedImageKernel hH m A B)) ↔ ∀ (x : S.carrier), ¬(SemanticCore.Mem S x B ∧ SemanticCore.Mem S (kPair hH (raise hH m x) z) A)

noncomputable def NFChoice.Foundation.NFStandard.raisedImageObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A B : S.carrier) : S.carrier

Raised-coordinate image: existentially quantify raise m x in a relation.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_raisedImageObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (m : ℕ) (A B z : S.carrier) : SemanticCore.Mem S z (raisedImageObj hH m A B) ↔ ∃ (x : S.carrier), SemanticCore.Mem S x B ∧ SemanticCore.Mem S (kPair hH (raise hH m x) z) A

noncomputable def NFChoice.Foundation.NFStandard.composeObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B : S.carrier) : S.carrier

Relational composition, defined from insertion and image as in df-cok.

Equations

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

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_composeObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B a b : S.carrier) : SemanticCore.Mem S (kPair hH a b) (composeObj hH A B) ↔ ∃ (x : S.carrier), SemanticCore.Mem S (kPair hH a x) B ∧ SemanticCore.Mem S (kPair hH x b) A