Nuprl Lemma : Form_ind_wf
∀[C,A:Type]. ∀[R:A ⟶ Form(C) ⟶ ℙ]. ∀[v:Form(C)]. ∀[Var:name:Atom ⟶ {x:A| R[x;Vname]} ].
∀[Const:value:C ⟶ {x:A| R[x;Const(value)]} ]. ∀[Set:var:Atom
                                                    ⟶ phi:Form(C)
                                                    ⟶ {x:A| R[x;phi]} 
                                                    ⟶ {x:A| R[x;{var | phi}]} ]. ∀[Equal:left:Form(C)
                                                                                         ⟶ right:Form(C)
                                                                                         ⟶ {x:A| R[x;left]} 
                                                                                         ⟶ {x:A| R[x;right]} 
                                                                                         ⟶ {x:A| R[x;left = right]} ].
∀[Member:element:Form(C) ⟶ set:Form(C) ⟶ {x:A| R[x;element]}  ⟶ {x:A| R[x;set]}  ⟶ {x:A| R[x;element ∈ set]} ].
∀[And:left:Form(C) ⟶ right:Form(C) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left ∧ right)]} ].
∀[Or:left:Form(C) ⟶ right:Form(C) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left ∨ right]} ].
∀[Not:body:Form(C) ⟶ {x:A| R[x;body]}  ⟶ {x:A| R[x;¬(body)]} ]. ∀[All:var:Atom
                                                                      ⟶ body:Form(C)
                                                                      ⟶ {x:A| R[x;body]} 
                                                                      ⟶ {x:A| R[x;∀var. body]} ].
∀[Exists:var:Atom ⟶ body:Form(C) ⟶ {x:A| R[x;body]}  ⟶ {x:A| R[x;∃var. body]} ].
  (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])  ∈ {x:A| R[x;v]} )
Proof
Definitions occuring in Statement : 
Form_ind: Form_ind, 
FormExists: ∃var. body
, 
FormAll: ∀var. body
, 
FormNot: ¬(body)
, 
FormOr: left ∨ right
, 
FormAnd: left ∧ right)
, 
FormMember: element ∈ set
, 
FormEqual: left = right
, 
FormSet: {var | phi}
, 
FormConst: Const(value)
, 
FormVar: Vname
, 
Form: Form(C)
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
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
, 
set: {x:A| B[x]} 
, 
function: x:A ⟶ B[x]
, 
atom: Atom
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
Form_ind: Form_ind, 
so_apply: x[s1;s2;s3]
, 
so_apply: x[s1;s2]
, 
so_apply: x[s1;s2;s3;s4]
, 
so_apply: x[s]
, 
Form-definition, 
Form-induction, 
uniform-comp-nat-induction, 
Form-ext, 
eq_atom: x =a y
, 
btrue: tt
, 
it: ⋅
, 
bfalse: ff
, 
bool_cases_sqequal, 
eqff_to_assert, 
any: any x
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
has-value: (a)↓
, 
so_lambda: so_lambda4, 
so_lambda: λ2x.t[x]
, 
uimplies: b supposing a
, 
subtype_rel: A ⊆r B
, 
prop: ℙ
, 
guard: {T}
Lemmas referenced : 
Form-definition, 
has-value_wf_base, 
is-exception_wf, 
lifting-strict-atom_eq, 
strict4-decide, 
Form_wf, 
istype-atom, 
FormVar_wf, 
FormConst_wf, 
FormSet_wf, 
FormEqual_wf, 
FormMember_wf, 
FormAnd_wf, 
FormOr_wf, 
FormNot_wf, 
FormAll_wf, 
FormExists_wf, 
all_wf, 
set_wf, 
subtype_rel_function, 
subtype_rel_self, 
istype-universe, 
Form-induction, 
uniform-comp-nat-induction, 
Form-ext, 
bool_cases_sqequal, 
eqff_to_assert
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
sqequalRule, 
Error :memTop, 
inhabitedIsType, 
hypothesis, 
lambdaFormation_alt, 
thin, 
sqequalSqle, 
divergentSqle, 
callbyvalueDecide, 
sqequalHypSubstitution, 
hypothesisEquality, 
unionElimination, 
sqleReflexivity, 
equalityIstype, 
equalityTransitivity, 
equalitySymmetry, 
dependent_functionElimination, 
independent_functionElimination, 
introduction, 
decideExceptionCases, 
axiomSqleEquality, 
exceptionSqequal, 
baseApply, 
closedConclusion, 
baseClosed, 
extract_by_obid, 
isectElimination, 
independent_isectElimination, 
lambdaEquality_alt, 
isectIsType, 
because_Cache, 
functionIsType, 
universeIsType, 
universeEquality, 
setIsType, 
applyEquality, 
functionEquality, 
setEquality, 
instantiate, 
functionExtensionality, 
atomEquality, 
setElimination, 
rename, 
dependent_set_memberEquality_alt
Latex:
\mforall{}[C,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  Form(C)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:Form(C)].  \mforall{}[Var:name:Atom  {}\mrightarrow{}  \{x:A|  R[x;Vname]\}  ].
\mforall{}[Const:value:C  {}\mrightarrow{}  \{x:A|  R[x;Const(value)]\}  ].  \mforall{}[Set:var:Atom
                                                                                                        {}\mrightarrow{}  phi:Form(C)
                                                                                                        {}\mrightarrow{}  \{x:A|  R[x;phi]\} 
                                                                                                        {}\mrightarrow{}  \{x:A|  R[x;\{var  |  phi\}]\}  ].
\mforall{}[Equal:left:Form(C)
                {}\mrightarrow{}  right:Form(C)
                {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                {}\mrightarrow{}  \{x:A|  R[x;left  =  right]\}  ].  \mforall{}[Member:element:Form(C)
                                                                                              {}\mrightarrow{}  set:Form(C)
                                                                                              {}\mrightarrow{}  \{x:A|  R[x;element]\} 
                                                                                              {}\mrightarrow{}  \{x:A|  R[x;set]\} 
                                                                                              {}\mrightarrow{}  \{x:A|  R[x;element  \mmember{}  set]\}  ].
\mforall{}[And:left:Form(C)
            {}\mrightarrow{}  right:Form(C)
            {}\mrightarrow{}  \{x:A|  R[x;left]\} 
            {}\mrightarrow{}  \{x:A|  R[x;right]\} 
            {}\mrightarrow{}  \{x:A|  R[x;left  \mwedge{}  right)]\}  ].  \mforall{}[Or:left:Form(C)
                                                                                    {}\mrightarrow{}  right:Form(C)
                                                                                    {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                    {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                    {}\mrightarrow{}  \{x:A|  R[x;left  \mvee{}  right]\}  ].  \mforall{}[Not:body:Form(C)
                                                                                                                                                            {}\mrightarrow{}  \{x:A|  R[x;body]\} 
                                                                                                                                                            {}\mrightarrow{}  \{x:A| 
                                                                                                                                                                    R[x;\mneg{}(body)]\}  ].
\mforall{}[All:var:Atom  {}\mrightarrow{}  body:Form(C)  {}\mrightarrow{}  \{x:A|  R[x;body]\}    {}\mrightarrow{}  \{x:A|  R[x;\mforall{}var.  body]\}  ].
\mforall{}[Exists:var:Atom  {}\mrightarrow{}  body:Form(C)  {}\mrightarrow{}  \{x:A|  R[x;body]\}    {}\mrightarrow{}  \{x:A|  R[x;\mexists{}var.  body]\}  ].
    (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{}  \{x:A|  R[x;v]\}  )
Date html generated:
2020_05_20-AM-09_12_23
Last ObjectModification:
2020_01_24-PM-01_52_09
Theory : PZF
Home
Index