Nuprl Lemma : int_formula_ind_wf_simple
∀[A:Type]. ∀[v:int_formula()]. ∀[less,le,eq:left:int_term() ⟶ right:int_term() ⟶ A].
∀[and,or,implies:left:int_formula() ⟶ right:int_formula() ⟶ A ⟶ A ⟶ A]. ∀[not:form:int_formula() ⟶ A ⟶ A].
(int_formula_ind(v;
intformless(left,right)⇒ less[left;right];
intformle(left,right)⇒ le[left;right];
intformeq(left,right)⇒ eq[left;right];
intformand(left,right)⇒ rec1,rec2.and[left;right;rec1;rec2];
intformor(left,right)⇒ rec3,rec4.or[left;right;rec3;rec4];
intformimplies(left,right)⇒ rec5,rec6.implies[left;right;rec5;rec6];
intformnot(form)⇒ rec7.not[form;rec7]) ∈ A)
Proof
Definitions occuring in Statement :
int_formula_ind: int_formula_ind,
int_formula: int_formula(),
int_term: int_term(),
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
prop: ℙ,
uimplies: b supposing a,
true: True,
so_lambda: λ2x.t[x],
so_apply: x[s],
all: ∀x:A. B[x]
Lemmas referenced :
int_formula_ind_wf,
true_wf,
int_formula_wf,
subtype_rel_function,
subtype_rel_self,
int_term_wf,
subtype_rel_dep_function,
istype-universe
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
Error :lambdaEquality_alt,
Error :universeIsType,
functionExtensionality,
applyEquality,
because_Cache,
setEquality,
independent_isectElimination,
Error :dependent_set_memberEquality_alt,
natural_numberEquality,
functionEquality,
Error :inhabitedIsType,
Error :lambdaFormation_alt,
Error :setIsType,
setElimination,
rename,
applyLambdaEquality,
Error :functionIsType,
instantiate,
universeEquality
Latex:
\mforall{}[A:Type]. \mforall{}[v:int\_formula()]. \mforall{}[less,le,eq:left:int\_term() {}\mrightarrow{} right:int\_term() {}\mrightarrow{} A].
\mforall{}[and,or,implies:left:int\_formula() {}\mrightarrow{} right:int\_formula() {}\mrightarrow{} A {}\mrightarrow{} A {}\mrightarrow{} A]. \mforall{}[not:form:int\_formula()
{}\mrightarrow{} A
{}\mrightarrow{} A].
(int\_formula\_ind(v;
intformless(left,right){}\mRightarrow{} less[left;right];
intformle(left,right){}\mRightarrow{} le[left;right];
intformeq(left,right){}\mRightarrow{} eq[left;right];
intformand(left,right){}\mRightarrow{} rec1,rec2.and[left;right;rec1;rec2];
intformor(left,right){}\mRightarrow{} rec3,rec4.or[left;right;rec3;rec4];
intformimplies(left,right){}\mRightarrow{} rec5,rec6.implies[left;right;rec5;rec6];
intformnot(form){}\mRightarrow{} rec7.not[form;rec7]) \mmember{} A)
Date html generated:
2019_06_20-PM-00_46_36
Last ObjectModification:
2019_01_12-AM-10_32_29
Theory : omega
Home
Index