Nuprl Lemma : Form_ind_wf_simple
∀[C,A:Type]. ∀[v:Form(C)]. ∀[Var:name:Atom ⟶ A]. ∀[Const:value:C ⟶ A]. ∀[Set:var:Atom ⟶ phi:Form(C) ⟶ A ⟶ A].
∀[Equal,Member,And,Or:left:Form(C) ⟶ right:Form(C) ⟶ A ⟶ A ⟶ A]. ∀[Not:body:Form(C) ⟶ A ⟶ A].
∀[All,Exists:var:Atom ⟶ body:Form(C) ⟶ A ⟶ A].
(Form_ind(v;
FormVar(name)
⇒ Var[name];
FormConst(value)
⇒ Const[value];
FormSet(var,phi)
⇒ rec1.Set[var;phi;rec1];
FormEqual(left,right)
⇒ rec2,rec3.Equal[left;right;rec2;rec3];
FormMember(element,set)
⇒ rec4,rec5.Member[element;set;rec4;rec5];
FormAnd(left,right)
⇒ rec6,rec7.And[left;right;rec6;rec7];
FormOr(left,right)
⇒ rec8,rec9.Or[left;right;rec8;rec9];
FormNot(body)
⇒ rec10.Not[body;rec10];
FormAll(var,body)
⇒ rec11.All[var;body;rec11];
FormExists(var,body)
⇒ rec12.Exists[var;body;rec12]) ∈ A)
Proof
Definitions occuring in Statement :
Form_ind: Form_ind,
Form: Form(C)
,
uall: ∀[x:A]. B[x]
,
so_apply: x[s1;s2;s3;s4]
,
so_apply: x[s1;s2;s3]
,
so_apply: x[s1;s2]
,
so_apply: x[s]
,
member: t ∈ T
,
function: x:A ⟶ B[x]
,
atom: Atom
,
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
,
true: True
,
prop: ℙ
,
so_lambda: λ2x.t[x]
,
so_apply: x[s]
,
uimplies: b supposing a
,
all: ∀x:A. B[x]
,
guard: {T}
Lemmas referenced :
Form_ind_wf,
true_wf,
Form_wf,
subtype_rel_dep_function,
set_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
lambdaEquality,
cumulativity,
functionExtensionality,
applyEquality,
dependent_set_memberEquality,
natural_numberEquality,
because_Cache,
functionEquality,
setEquality,
independent_isectElimination,
lambdaFormation,
setElimination,
rename,
equalityTransitivity,
equalitySymmetry,
atomEquality,
universeEquality
Latex:
\mforall{}[C,A:Type]. \mforall{}[v:Form(C)]. \mforall{}[Var:name:Atom {}\mrightarrow{} A]. \mforall{}[Const:value:C {}\mrightarrow{} A]. \mforall{}[Set:var:Atom
{}\mrightarrow{} phi:Form(C)
{}\mrightarrow{} A
{}\mrightarrow{} A].
\mforall{}[Equal,Member,And,Or:left:Form(C) {}\mrightarrow{} right:Form(C) {}\mrightarrow{} A {}\mrightarrow{} A {}\mrightarrow{} A]. \mforall{}[Not:body:Form(C) {}\mrightarrow{} A {}\mrightarrow{} A].
\mforall{}[All,Exists:var:Atom {}\mrightarrow{} body:Form(C) {}\mrightarrow{} A {}\mrightarrow{} A].
(Form\_ind(v;
FormVar(name){}\mRightarrow{} Var[name];
FormConst(value){}\mRightarrow{} Const[value];
FormSet(var,phi){}\mRightarrow{} rec1.Set[var;phi;rec1];
FormEqual(left,right){}\mRightarrow{} rec2,rec3.Equal[left;right;rec2;rec3];
FormMember(element,set){}\mRightarrow{} rec4,rec5.Member[element;set;rec4;rec5];
FormAnd(left,right){}\mRightarrow{} rec6,rec7.And[left;right;rec6;rec7];
FormOr(left,right){}\mRightarrow{} rec8,rec9.Or[left;right;rec8;rec9];
FormNot(body){}\mRightarrow{} rec10.Not[body;rec10];
FormAll(var,body){}\mRightarrow{} rec11.All[var;body;rec11];
FormExists(var,body){}\mRightarrow{} rec12.Exists[var;body;rec12]) \mmember{} A)
Date html generated:
2018_05_21-PM-11_26_28
Last ObjectModification:
2017_10_10-PM-04_37_28
Theory : PZF
Home
Index