Nuprl Lemma : formula_ind_wf

[A:Type]. ∀[R:A ⟶ formula() ⟶ ℙ]. ∀[v:formula()]. ∀[var:name:Atom ⟶ {x:A| R[x;pvar(name)]} ].
[not:sub:formula() ⟶ {x:A| R[x;sub]}  ⟶ {x:A| R[x;pnot(sub)]} ]. ∀[and:left:formula()
                                                                        ⟶ right:formula()
                                                                        ⟶ {x:A| R[x;left]} 
                                                                        ⟶ {x:A| R[x;right]} 
                                                                        ⟶ {x:A| R[x;pand(left;right)]} ].
[or:left:formula() ⟶ right:formula() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;por(left;right)]} ].
[imp:left:formula() ⟶ right:formula() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;pimp(left;right)]} ].
  (formula_ind(v;
               pvar(name) var[name];
               pnot(sub) rec1.not[sub;rec1];
               pand(left,right) rec2,rec3.and[left;right;rec2;rec3];
               por(left,right) rec4,rec5.or[left;right;rec4;rec5];
               pimp(left,right) rec6,rec7.imp[left;right;rec6;rec7])  ∈ {x:A| R[x;v]} )


Proof




Definitions occuring in Statement :  formula_ind: formula_ind pimp: pimp(left;right) por: por(left;right) pand: pand(left;right) pnot: pnot(sub) pvar: pvar(name) formula: formula() uall: [x:A]. B[x] prop: so_apply: x[s1;s2;s3;s4] 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 formula_ind: formula_ind so_apply: x[s1;s2;s3;s4] so_apply: x[s1;s2] so_apply: x[s] formula-definition formula-induction uniform-comp-nat-induction formula-ext eq_atom: =a y btrue: tt it: bfalse: ff bool_cases_sqequal eqff_to_assert any: any x all: x:A. B[x] implies:  Q has-value: (a)↓ so_lambda: so_lambda4 so_lambda: λ2x.t[x] uimplies: supposing a subtype_rel: A ⊆B prop: guard: {T}
Lemmas referenced :  formula-definition has-value_wf_base is-exception_wf lifting-strict-atom_eq strict4-decide istype-atom pvar_wf pnot_wf pand_wf por_wf pimp_wf formula_wf all_wf set_wf subtype_rel_function subtype_rel_self istype-universe formula-induction uniform-comp-nat-induction formula-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 functionIsType universeIsType universeEquality setIsType because_Cache applyEquality functionEquality setEquality instantiate functionExtensionality atomEquality setElimination rename dependent_set_memberEquality_alt

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  formula()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:formula()].  \mforall{}[var:name:Atom  {}\mrightarrow{}  \{x:A|  R[x;pvar(name)]\}  ].
\mforall{}[not:sub:formula()  {}\mrightarrow{}  \{x:A|  R[x;sub]\}    {}\mrightarrow{}  \{x:A|  R[x;pnot(sub)]\}  ].  \mforall{}[and:left:formula()
                                                                                                                                                {}\mrightarrow{}  right:formula()
                                                                                                                                                {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                                                                                {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                                                                                {}\mrightarrow{}  \{x:A| 
                                                                                                                                                        R[x;pand(left;right)]\}  ]\000C.
\mforall{}[or:left:formula()
          {}\mrightarrow{}  right:formula()
          {}\mrightarrow{}  \{x:A|  R[x;left]\} 
          {}\mrightarrow{}  \{x:A|  R[x;right]\} 
          {}\mrightarrow{}  \{x:A|  R[x;por(left;right)]\}  ].  \mforall{}[imp:left:formula()
                                                                                        {}\mrightarrow{}  right:formula()
                                                                                        {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                        {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                        {}\mrightarrow{}  \{x:A|  R[x;pimp(left;right)]\}  ].
    (formula\_ind(v;
                              pvar(name){}\mRightarrow{}  var[name];
                              pnot(sub){}\mRightarrow{}  rec1.not[sub;rec1];
                              pand(left,right){}\mRightarrow{}  rec2,rec3.and[left;right;rec2;rec3];
                              por(left,right){}\mRightarrow{}  rec4,rec5.or[left;right;rec4;rec5];
                              pimp(left,right){}\mRightarrow{}  rec6,rec7.imp[left;right;rec6;rec7])    \mmember{}  \{x:A|  R[x;v]\}  )



Date html generated: 2020_05_20-AM-08_18_38
Last ObjectModification: 2020_01_24-PM-02_36_12

Theory : general


Home Index