OAI/Computability/MinUncut/Search/UniformQuantifier.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MinUncut.Preprocess.UEncoding.Map.ofEqline 12 - lemma
OAI.MinUncut.Preprocess.UEncoding.map_trueline 17 - lemma
OAI.MinUncut.Preprocess.UEncoding.map_falseline 19 - lemma
OAI.MinUncut.Preprocess.UEncoding.map_forallline 22 - lemma
OAI.MinUncut.Preprocess.UEncoding.map_existsline 33 - def
OAI.MinUncut.Preprocess.UEncoding.Valueline 45 - lemma
OAI.MinUncut.Preprocess.UEncoding.value_codeline 48 - lemma
OAI.MinUncut.Preprocess.UEncoding.value_constline 50 - lemma
OAI.MinUncut.Preprocess.UEncoding.Value.compline 52 - lemma
OAI.MinUncut.Preprocess.UEncoding.Value.mapline 59 - lemma
OAI.MinUncut.Preprocess.UEncoding.Value.map₂line 63 - lemma
OAI.MinUncut.Preprocess.UEncoding.value_sumline 70