### 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