theorem ISAR.HF_sound (t u : ISKSubtype) (h : OperEq t u) : ExtEq (decode_term t) (decode_term u)

theorem ISAR.HF_decode_eq (c1 c2 : HF) (h : ExtEq c1 c2) : OperEq (encode_raw c1) (encode_raw c2)

@[reducible, inline]

noncomputable abbrev ISAR.HF_Kernel : Kernel

The set-theoretic admissible semantic kernel. Packages hereditarily finite sets as a decoder/view over the ISAR stack.

Equations

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

theorem ISAR.HF_Kernel_factorization (f : KernelHom HF_Kernel ISAR_Kernel) (c : HF) : OperEq (f.hom c) (encode_raw c)

ZFC Interpretation Theorem: The hereditarily finite set fragment admits a faithful interpretation into the ISAR invariant quotient, and the induced semantic kernel HF_Kernel factors uniquely through ISAR_Kernel in the category of admissible kernels.