Some facts about UUF.*_ids.

theorem Cedar.Thm.prefix_ne_at_index {p₁ p₂ x y : String} {i : Nat} (h₁ : i < p₁.toList.length) (h₂ : i < p₂.toList.length) (hₙ : p₁.toList[i]? ≠ p₂.toList[i]?) : (p₁ ++ x).toList ≠ (p₂ ++ y).toList

def Cedar.Thm.commandGen_prefix_no_confusion____ : Lean.ParserDescr

Equations

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

theorem Cedar.Thm.attrs_ancs_no_confusion_prefix {x✝ y✝ : String} : ("attrs[" ++ x✝).toList ≠ ("ancs[" ++ y✝).toList

theorem Cedar.Thm.attrs_tag_keys_no_confusion_prefix {x✝ y✝ : String} : ("attrs[" ++ x✝).toList ≠ ("tagKeys[" ++ y✝).toList

theorem Cedar.Thm.attrs_tag_vals_no_confusion_prefix {x✝ y✝ : String} : ("attrs[" ++ x✝).toList ≠ ("tagVals[" ++ y✝).toList

theorem Cedar.Thm.tag_vals_tag_keys_no_confusion_prefix {x✝ y✝ : String} : ("tagVals[" ++ x✝).toList ≠ ("tagKeys[" ++ y✝).toList

theorem Cedar.Thm.tag_keys_ancs_no_confusion_prefix {x✝ y✝ : String} : ("tagKeys[" ++ x✝).toList ≠ ("ancs[" ++ y✝).toList

theorem Cedar.Thm.tag_vals_ancs_no_confusion_prefix {x✝ y✝ : String} : ("tagVals[" ++ x✝).toList ≠ ("ancs[" ++ y✝).toList

theorem Cedar.Thm.uuf_attrs_ancs_no_confusion {ety₁ ety₂ ancTy : Spec.EntityType} : SymCC.UUF.attrsId ety₁ ≠ SymCC.UUF.ancsId ety₂ ancTy

theorem Cedar.Thm.uuf_attrs_tag_keys_no_confusion {ety₁ ety₂ : Spec.EntityType} : SymCC.UUF.attrsId ety₁ ≠ SymCC.UUF.tagKeysId ety₂

theorem Cedar.Thm.uuf_attrs_tag_vals_no_confusion {ety₁ ety₂ : Spec.EntityType} : SymCC.UUF.attrsId ety₁ ≠ SymCC.UUF.tagValsId ety₂

theorem Cedar.Thm.uuf_tag_vals_tag_keys_no_confusion {ety₁ ety₂ : Spec.EntityType} : SymCC.UUF.tagValsId ety₁ ≠ SymCC.UUF.tagKeysId ety₂

theorem Cedar.Thm.uuf_tag_keys_ancs_no_confusion {ety₁ ety₂ ancTy : Spec.EntityType} : SymCC.UUF.tagKeysId ety₁ ≠ SymCC.UUF.ancsId ety₂ ancTy

theorem Cedar.Thm.uuf_tag_vals_ancs_no_confusion {ety₁ ety₂ ancTy : Spec.EntityType} : SymCC.UUF.tagValsId ety₁ ≠ SymCC.UUF.ancsId ety₂ ancTy