| NBG-031 |
| Identifier |
def_ord |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/ord-pred.html}{\mathrm{Ord}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/ord-pred.html}{\mathrm{Ord}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_ord\_def}} \)
|
| SML Kernel AST |
(Pi (A : Class) -> (Sigma (_ : (Pi (_ : (Id Prop (Ord A) true)) -> (Sigma (_ : (Id Prop (Trans A) true)) * (Pi (B : Class) -> (Pi (_ : (Id Prop ((In B) A) true)) -> (Id Prop (Trans B) true)))))) * (Pi (_ : (Sigma (_ : (Id Prop (Trans A) true)) * (Pi (B : Class) -> (Pi (_ : (Id Prop ((In B) A) true)) -> (Id Prop (Trans B) true))))) -> (Id Prop (Ord A) true)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-032 |
| Identifier |
ax_global_choice |
| Classification |
Irreducible MK/NBG Axiom |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/eps-binder.html}{\mathsf{choice}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_global\_choice}} \)
|
| SML Kernel AST |
(Pi (A : Class) -> (Pi (_ : (Sigma (x : Class) * (Id Prop ((In x) A) true))) -> (Id Prop ((In (choice A)) A) true))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-033 |
| Identifier |
thm_subset_refl |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hz}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/variables.html}{\mathsf{hz}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (X : Class) -> (Pi (z : Class) -> (Pi (_ : (Id Prop ((In z) X) true)) -> (Id Prop ((In z) X) true)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-034 |
| Identifier |
thm_subset_trans |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{h1}} \href{symbols/typing-colon.html}{:} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{h2}} \href{symbols/typing-colon.html}{:} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hz}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{h2}} \href{symbols/variables.html}{z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{h1}} \href{symbols/variables.html}{z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hz}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (X : Class) -> (Pi (Y : Class) -> (Pi (Z : Class) -> (Pi (_ : (Pi (z : Class) -> (Pi (_ : (Id Prop ((In z) X) true)) -> (Id Prop ((In z) Y) true)))) -> (Pi (_ : (Pi (z : Class) -> (Pi (_ : (Id Prop ((In z) Y) true)) -> (Id Prop ((In z) Z) true)))) -> (Pi (z : Class) -> (Pi (_ : (Id Prop ((In z) X) true)) -> (Id Prop ((In z) Z) true)))))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-035 |
| Identifier |
def_dunaev_opair |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{def\_dunaev\_opair\_witness}} \)
|
| SML Kernel AST |
(Pi (a : Class) -> (Pi (b : Class) -> (Id Class ((Pair a) b) ((DunaevPair a) b)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-036 |
| Identifier |
def_relational_func |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/func-pred.html}{\mathsf{function}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{z} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/func-pred.html}{\mathsf{function}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{F} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_relational\_func\_def}} \)
|
| SML Kernel AST |
(Pi (F : Class) -> (Sigma (_ : (Pi (_ : (Id Prop (Func F) true)) -> (Pi (x : Class) -> (Pi (y : Class) -> (Pi (z : Class) -> (Pi (_ : (Sigma (_ : (Id Prop ((In ((DunaevPair x) y)) F) true)) * (Id Prop ((In ((DunaevPair x) z)) F) true))) -> (Id Class y z))))))) * (Pi (_ : (Pi (x : Class) -> (Pi (y : Class) -> (Pi (z : Class) -> (Pi (_ : (Sigma (_ : (Id Prop ((In ((DunaevPair x) y)) F) true)) * (Id Prop ((In ((DunaevPair x) z)) F) true))) -> (Id Class y z)))))) -> (Id Prop (Func F) true)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-037 |
| Identifier |
thm_zero_is_nat |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/numeral-0.html}{0} \href{symbols/eq-pred.html}{=} \href{symbols/numeral-0.html}{0} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/eq-pred.html}{\mathsf{refl}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/numeral-0.html}{0} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Id Nat 0 0) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-038 |
| Identifier |
thm_succ_preserves_nat |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/eq-pred.html}{\mathsf{refl}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (n : Nat) -> (Id Nat (succ n) (succ n))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-039 |
| Identifier |
thm_zero_not_succ |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{h} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/numeral-0.html}{0} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/bot-const.html}{\bot} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{h} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/numeral-0.html}{0} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_peano\_zero\_not\_succ}} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{h} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (n : Nat) -> (Pi (h : (Id Nat (succ n) 0)) -> False)) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-040 |
| Identifier |
thm_succ_injective |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{m} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{h} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{m} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{m} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{m} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{h} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{m} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_peano\_succ\_inj}} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{m} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{h} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (n : Nat) -> (Pi (m : Nat) -> (Pi (h : (Id Nat (succ n) (succ m))) -> (Id Nat n m)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-041 |
| Identifier |
thm_add_zero_left |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/eq-pred.html}{\mathsf{refl}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (n : Nat) -> (Id Nat n n)) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-042 |
| Identifier |
thm_mathematical_induction |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/prop-bool.html}{\mathsf{Prop}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{base}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/numeral-0.html}{0} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{step}} \href{symbols/typing-colon.html}{:} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ih}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/prop-bool.html}{\mathsf{Prop}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{base}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/numeral-0.html}{0} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{step}} \href{symbols/typing-colon.html}{:} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ih}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/omega-const.html}{\mathsf{succ}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{n} \href{symbols/typing-colon.html}{:} \href{symbols/omega-const.html}{\mathsf{Nat}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/omega-const.html}{\mathsf{nat\_rec}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{P} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{\mathsf{base}} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{\mathsf{step}} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{n} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (P : (Pi (_ : Nat) -> Prop)) -> (Pi (base : (P 0)) -> (Pi (step : (Pi (n : Nat) -> (Pi (ih : (P n)) -> (P (succ n))))) -> (Pi (n : Nat) -> (P n))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-043 |
| Identifier |
thm_v_ind |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_intro}} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_universal\_class\_def}} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{\mathsf{refl}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/emptyset-const.html}{\emptyset} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{ax\_empty\_set}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hyInV}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_universal\_class\_def}} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{\mathsf{refl}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/binunion-op.html}{\mathsf{SuccOrd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ord\_succ\_set}} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_universal\_class\_def}} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{\mathsf{refl}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hyInV}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Id Prop (Ind V) true) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-044 |
| Identifier |
thm_omega_def |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \)
|
| SML Kernel AST |
(Pi (x : Class) -> (Sigma (_ : (Pi (_ : (Id Prop ((In x) omega) true)) -> (Pi (Q : Class) -> (Pi (_ : (Id Prop (Ind Q) true)) -> (Id Prop ((In x) Q) true))))) * (Pi (_ : (Pi (Q : Class) -> (Pi (_ : (Id Prop (Ind Q) true)) -> (Id Prop ((In x) Q) true)))) -> (Id Prop ((In x) omega) true)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-045 |
| Identifier |
thm_omega_set |
| Classification |
Irreducible MK/NBG Axiom |
| Statement (Type) |
0\(\href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_omega\_set}} \)
|
| SML Kernel AST |
(Id Prop (Set omega) true) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-046 |
| Identifier |
thm_omega_ind |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_intro}} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/emptyset-const.html}{\emptyset} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/typing-colon.html}{:} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_elim}} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hyInOmega}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/binunion-op.html}{\mathsf{SuccOrd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/typing-colon.html}{:} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_elim}} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hyInOmega}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Id Prop (Ind omega) true) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-047 |
| Identifier |
thm_tr_omega |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/trans-pred.html}{\mathrm{Tr}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_omega\_trans\_from\_ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_intro}} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/emptyset-const.html}{\emptyset} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/typing-colon.html}{:} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_elim}} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hyInOmega}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/binunion-op.html}{\mathsf{SuccOrd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/typing-colon.html}{:} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_elim}} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hyInOmega}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{ax\_omega\_elements\_trans}} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Id Prop (Trans omega) true) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-048 |
| Identifier |
thm_ord_omega |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/ord-pred.html}{\mathrm{Ord}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_ord\_def}} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_omega\_trans\_from\_ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_intro}} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/emptyset-const.html}{\emptyset} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/typing-colon.html}{:} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_elim}} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hyInOmega}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/binunion-op.html}{\mathsf{SuccOrd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/typing-colon.html}{:} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_elim}} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hyInOmega}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{ax\_omega\_elements\_trans}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{\mathsf{ax\_omega\_elements\_trans}} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Id Prop (Ord omega) true) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-049 |
| Identifier |
thm_omega_in_on |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/in-pred.html}{\in} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_on\_intro}} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/variables.html}{\mathsf{plan\_omega\_set}} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_ord\_def}} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_omega\_trans\_from\_ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_intro}} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/emptyset-const.html}{\emptyset} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/typing-colon.html}{:} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_elim}} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hyInOmega}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/binunion-op.html}{\mathsf{SuccOrd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/typing-colon.html}{:} \href{symbols/ind-pred.html}{\mathrm{Ind}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ind\_elim}} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_omega\_def}} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hyInOmega}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{Q} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIndQ}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{ax\_omega\_elements\_trans}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{\mathsf{ax\_omega\_elements\_trans}} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Id Prop ((In omega) On) true) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-050 |
| Identifier |
thm_on_ind |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/emptyset-const.html}{\emptyset} \href{symbols/in-pred.html}{\in} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/in-pred.html}{\in} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/binunion-op.html}{\mathsf{SuccOrd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_on\_intro}} \href{symbols/emptyset-const.html}{\emptyset} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/variables.html}{\mathsf{ax\_empty\_set}} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{\mathsf{ax\_empty\_ord}} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/in-pred.html}{\in} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_on\_intro}} \href{symbols/binunion-op.html}{\mathsf{SuccOrd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ord\_succ\_set}} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_on\_elim}} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_ord\_succ\_ord}} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_on\_elim}} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \)
|
| SML Kernel AST |
(Sigma (_ : (Id Prop ((In EmptySet) On) true)) * (Pi (a : Class) -> (Pi (_ : (Id Prop ((In a) On) true)) -> (Id Prop ((In (SuccOrd a)) On) true)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-051 |
| Identifier |
def_isCard |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/card-op.html}{\mathsf{CardOf}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/card-op.html}{\mathsf{CardOf}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{K} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_card\_def}} \)
|
| SML Kernel AST |
(Pi (C : Class) -> (Sigma (_ : (Pi (_ : (Card C)) -> (Sigma (K : Class) * (Id Class (CardOf K) C)))) * (Pi (_ : (Sigma (K : Class) * (Id Class (CardOf K) C))) -> (Card C)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-052 |
| Identifier |
thm_omega_card |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_card\_def}} \href{symbols/omega-const.html}{\omega} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/omega-const.html}{\omega} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{\mathsf{ax\_cardof\_omega}} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Card omega) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-053 |
| Identifier |
thm_on_card |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_card\_def}} \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/on-const.html}{\mathbf{On}} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{\mathsf{ax\_cardof\_on}} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Card On) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-054 |
| Identifier |
thm_v_not_card |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/neg-conn.html}{\neg} \href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hCardV}} \href{symbols/typing-colon.html}{:} \href{symbols/card-pred.html}{\mathrm{Card}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_cardof\_never\_v}} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_card\_def}} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hCardV}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{plan\_card\_def}} \href{symbols/universal-class-const.html}{\mathbf{V}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hCardV}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (_ : (Card V)) -> False) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-055 |
| Identifier |
ax_tarski_universes |
| Classification |
Irreducible MK/NBG Axiom |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/universe-pred.html}{\mathsf{universe}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{X} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{U} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_tarski\_axm}} \)
|
| SML Kernel AST |
(Pi (X : Class) -> (Pi (_ : (Id Prop (Set X) true)) -> (Sigma (U : Class) * (Sigma (_ : (Universe U)) * (Sigma (_ : (Id Prop ((In X) U) true)) * (Id Prop (Set U) true)))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-056 |
| Identifier |
def_binary_union |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/binunion-op.html}{\cup} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/typing-colon.html}{:} \href{symbols/prop-bool.html}{\mathsf{Prop}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/typing-colon.html}{:} \href{symbols/prop-bool.html}{\mathsf{Prop}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/binunion-op.html}{\cup} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_bin\_union}} \)
|
| SML Kernel AST |
(Pi (A : Class) -> (Pi (B : Class) -> (Pi (z : Class) -> (Sigma (_ : (Pi (_ : (Id Prop ((In z) ((BinUnion A) B)) true)) -> (Pi (C : Prop) -> (Pi (_ : (Pi (_ : (Id Prop ((In z) A) true)) -> C)) -> (Pi (_ : (Pi (_ : (Id Prop ((In z) B) true)) -> C)) -> C))))) * (Pi (_ : (Pi (C : Prop) -> (Pi (_ : (Pi (_ : (Id Prop ((In z) A) true)) -> C)) -> (Pi (_ : (Pi (_ : (Id Prop ((In z) B) true)) -> C)) -> C)))) -> (Id Prop ((In z) ((BinUnion A) B)) true)))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-057 |
| Identifier |
def_binary_inter |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/bininter-op.html}{\cap} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/bininter-op.html}{\cap} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_bin\_inter}} \)
|
| SML Kernel AST |
(Pi (A : Class) -> (Pi (B : Class) -> (Pi (z : Class) -> (Sigma (_ : (Pi (_ : (Id Prop ((In z) ((BinInter A) B)) true)) -> (Sigma (_ : (Id Prop ((In z) A) true)) * (Id Prop ((In z) B) true)))) * (Pi (_ : (Sigma (_ : (Id Prop ((In z) A) true)) * (Id Prop ((In z) B) true))) -> (Id Prop ((In z) ((BinInter A) B)) true)))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-058 |
| Identifier |
def_unary_union |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/bigunion-op.html}{\bigcup} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/bigunion-op.html}{\bigcup} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_unary\_union}} \)
|
| SML Kernel AST |
(Pi (A : Class) -> (Pi (z : Class) -> (Sigma (_ : (Pi (_ : (Id Prop ((In z) (Union A)) true)) -> (Sigma (y : Class) * (Sigma (_ : (Id Prop ((In y) A) true)) * (Id Prop ((In z) y) true))))) * (Pi (_ : (Sigma (y : Class) * (Sigma (_ : (Id Prop ((In y) A) true)) * (Id Prop ((In z) y) true)))) -> (Id Prop ((In z) (Union A)) true))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-059 |
| Identifier |
def_unary_inter |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/biginter-op.html}{\bigcap} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{y} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{y} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/biginter-op.html}{\bigcap} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_unary\_inter}} \)
|
| SML Kernel AST |
(Pi (A : Class) -> (Pi (z : Class) -> (Sigma (_ : (Pi (_ : (Id Prop ((In z) (Inter A)) true)) -> (Pi (y : Class) -> (Pi (_ : (Id Prop ((In y) A) true)) -> (Id Prop ((In z) y) true))))) * (Pi (_ : (Pi (y : Class) -> (Pi (_ : (Id Prop ((In y) A) true)) -> (Id Prop ((In z) y) true)))) -> (Id Prop ((In z) (Inter A)) true))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-060 |
| Identifier |
def_singleton |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/singleton-op.html}{\{} \href{symbols/variables.html}{a} \href{symbols/singleton-op.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/singleton-op.html}{\{} \href{symbols/variables.html}{a} \href{symbols/singleton-op.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_singleton}} \)
|
| SML Kernel AST |
(Pi (a : Class) -> (Pi (z : Class) -> (Sigma (_ : (Pi (_ : (Id Prop ((In z) (Singleton a)) true)) -> (Sigma (_ : (Id Prop (Set a) true)) * (Id Class z a)))) * (Pi (_ : (Sigma (_ : (Id Prop (Set a) true)) * (Id Class z a))) -> (Id Prop ((In z) (Singleton a)) true))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-061 |
| Identifier |
def_upair |
| Classification |
Conservative Definition |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{a} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{b} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/upair-op.html}{\{} \href{symbols/variables.html}{a} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{b} \href{symbols/upair-op.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/typing-colon.html}{:} \href{symbols/prop-bool.html}{\mathsf{Prop}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/typing-colon.html}{:} \href{symbols/prop-bool.html}{\mathsf{Prop}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{a} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{b} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{z} \href{symbols/in-pred.html}{\in} \href{symbols/upair-op.html}{\{} \href{symbols/variables.html}{a} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{b} \href{symbols/upair-op.html}{\}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/variables.html}{\mathsf{plan\_upair}} \)
|
| SML Kernel AST |
(Pi (a : Class) -> (Pi (b : Class) -> (Pi (z : Class) -> (Sigma (_ : (Pi (_ : (Id Prop ((In z) ((UPair a) b)) true)) -> (Pi (C : Prop) -> (Pi (_ : (Pi (_ : (Id Class z a)) -> C)) -> (Pi (_ : (Pi (_ : (Id Class z b)) -> C)) -> C))))) * (Pi (_ : (Pi (C : Prop) -> (Pi (_ : (Pi (_ : (Id Class z a)) -> C)) -> (Pi (_ : (Pi (_ : (Id Class z b)) -> C)) -> C)))) -> (Id Prop ((In z) ((UPair a) b)) true)))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-062 |
| Identifier |
thm_russell_class_not_set |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{R} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{R} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{R} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{R} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/typing-colon.html}{:} \href{symbols/exists-binder.html}{\exists} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{R} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{R} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{R} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/set-pred.html}{\mathsf{set}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/neg-conn.html}{\neg} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{x} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{x} \href{symbols/in-pred.html}{\in} \href{symbols/variables.html}{R} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\langle } \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/in-pred.html}{\in} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hExists}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hIn}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (_ : (Sigma (R : Class) * (Sigma (_ : (Id Prop (Set R) true)) * (Pi (x : Class) -> (Sigma (_ : (Pi (_ : (Id Prop ((In x) R) true)) -> (Sigma (_ : (Id Prop (Set x) true)) * (Pi (_ : (Id Prop ((In x) x) true)) -> False)))) * (Pi (_ : (Sigma (_ : (Id Prop (Set x) true)) * (Pi (_ : (Id Prop ((In x) x) true)) -> False))) -> (Id Prop ((In x) R) true))))))) -> False) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-063 |
| Identifier |
thm_dunaev_tagged_pair_proj |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/pr1-op.html}{\mathrm{pr}_1} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/pr2-op.html}{\mathrm{pr}_2} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr1}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr2}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (A : Class) -> (Pi (B : Class) -> (Sigma (_ : (Id Class (DunaevPr1 ((DunaevPair A) B)) A)) * (Id Class (DunaevPr2 ((DunaevPair A) B)) B)))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|
| NBG-064 |
| Identifier |
thm_dunaev_pair_injectivity |
| Classification |
Derived Theorem (Constructive λ-Proof) |
| Statement (Type) |
0\(\href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/forall-binder.html}{\forall} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{D} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/impl-conn.html}{\rightarrow} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/and-conn.html}{\land} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/eq-pred.html}{=} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| Proof Program |
0\(\href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{D} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{hEq}} \href{symbols/typing-colon.html}{:} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/eq-pred.html}{=} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_eq\_trans}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/pr1-op.html}{\mathrm{pr}_1} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_eq\_trans}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/pr1-op.html}{\mathrm{pr}_1} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/pr1-op.html}{\mathrm{pr}_1} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_eq\_sym}} \href{symbols/pr1-op.html}{\mathrm{pr}_1} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr1}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr2}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_eq\_cong\_pr1}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hEq}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/fst-op.html}{\mathsf{fst}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr1}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr2}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_eq\_trans}} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/pr2-op.html}{\mathrm{pr}_2} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_eq\_trans}} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/pr2-op.html}{\mathrm{pr}_2} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/pr2-op.html}{\mathrm{pr}_2} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_eq\_sym}} \href{symbols/pr2-op.html}{\mathrm{pr}_2} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr1}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr2}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_eq\_cong\_pr2}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{C} \href{symbols/comma-delim.html}{,} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{\mathsf{hEq}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/snd-op.html}{\mathsf{snd}} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{A} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/delimiters-brackets.html}{(} \href{symbols/lambda-binder.html}{\lambda} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{B} \href{symbols/typing-colon.html}{:} \href{symbols/class-type.html}{\mathsf{Class}} \href{symbols/delimiters-brackets.html}{)} \href{symbols/dot-delim.html}{.} \href{symbols/antiquotation.html}{\langle } \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr1}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/comma-delim.html}{,} \href{symbols/delimiters-brackets.html}{(} \href{symbols/delimiters-brackets.html}{(} \href{symbols/variables.html}{\mathsf{ax\_dunaev\_pr2}} \href{symbols/variables.html}{A} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{B} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{C} \href{symbols/delimiters-brackets.html}{)} \href{symbols/variables.html}{D} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/antiquotation.html}{\rangle } \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \href{symbols/delimiters-brackets.html}{)} \)
|
| SML Kernel AST |
(Pi (A : Class) -> (Pi (B : Class) -> (Pi (C : Class) -> (Pi (D : Class) -> (Pi (_ : (Id Class ((DunaevPair A) B) ((DunaevPair C) D))) -> (Sigma (_ : (Id Class A C)) * (Id Class B D))))))) |
| Verification |
✔ Mechanically Type-Checked (DependentTypeChecker.check) |
|