Nuprl Lemma : int_formula_ind_wf
∀[A:Type]. ∀[R:A ⟶ int_formula() ⟶ ℙ]. ∀[v:int_formula()]. ∀[less:left:int_term()
⟶ right:int_term()
⟶ {x:A| R[x;(left "<" right)]} ].
∀[le:left:int_term() ⟶ right:int_term() ⟶ {x:A| R[x;left "≤" right]} ]. ∀[eq:left:int_term()
⟶ right:int_term()
⟶ {x:A| R[x;left "=" right]} ].
∀[and:left:int_formula() ⟶ right:int_formula() ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left "∧" right]}\000C ].
∀[or:left:int_formula() ⟶ right:int_formula() ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left "or" right]}\000C ].
∀[implies:left:int_formula()
⟶ right:int_formula()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;left "=>" right]} ]. ∀[not:form:int_formula() ⟶ {x:A| R[x;form]} ⟶ {x:A| R[x;"¬"form]} ].
(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]) ∈ {x:A| R[x;v]} )
Proof
Definitions occuring in Statement :
int_formula_ind: int_formula_ind,
intformnot: "¬"form,
intformimplies: left "=>" right,
intformor: left "or" right,
intformand: left "∧" right,
intformeq: left "=" right,
intformle: left "≤" right,
intformless: (left "<" right),
int_formula: int_formula(),
int_term: int_term(),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
int_formula_ind: int_formula_ind,
so_apply: x[s1;s2],
so_apply: x[s1;s2;s3;s4],
int_formula-definition,
int_formula-induction,
uniform-comp-nat-induction,
int_formula-ext,
eq_atom: x =a y,
btrue: tt,
it: ⋅,
bfalse: ff,
bool_cases_sqequal,
eqff_to_assert,
any: any x,
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
has-value: (a)↓,
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ,
guard: {T}
Lemmas referenced :
int_formula-definition,
istype-void,
has-value_wf_base,
is-exception_wf,
lifting-strict-atom_eq,
strict4-decide,
int_term_wf,
intformless_wf,
intformle_wf,
intformeq_wf,
intformand_wf,
intformor_wf,
intformimplies_wf,
intformnot_wf,
int_formula_wf,
all_wf,
set_wf,
subtype_rel_function,
subtype_rel_self,
istype-universe,
int_formula-induction,
uniform-comp-nat-induction,
int_formula-ext,
bool_cases_sqequal,
eqff_to_assert
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
cut,
sqequalRule,
Error :isect_memberEquality_alt,
voidElimination,
introduction,
extract_by_obid,
hypothesis,
Error :inhabitedIsType,
Error :lambdaFormation_alt,
thin,
sqequalSqle,
divergentSqle,
callbyvalueDecide,
sqequalHypSubstitution,
hypothesisEquality,
unionElimination,
sqleReflexivity,
Error :equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
decideExceptionCases,
axiomSqleEquality,
exceptionSqequal,
baseApply,
closedConclusion,
baseClosed,
isectElimination,
independent_isectElimination,
instantiate,
applyEquality,
Error :lambdaEquality_alt,
Error :isectIsType,
Error :functionIsType,
Error :universeIsType,
universeEquality,
because_Cache,
Error :setIsType,
functionEquality,
setEquality,
functionExtensionality,
setElimination,
rename,
Error :dependent_set_memberEquality_alt
Latex:
\mforall{}[A:Type]. \mforall{}[R:A {}\mrightarrow{} int\_formula() {}\mrightarrow{} \mBbbP{}]. \mforall{}[v:int\_formula()]. \mforall{}[less:left:int\_term()
{}\mrightarrow{} right:int\_term()
{}\mrightarrow{} \{x:A|
R[x;(left "<" right)]\} ].
\mforall{}[le:left:int\_term() {}\mrightarrow{} right:int\_term() {}\mrightarrow{} \{x:A| R[x;left "\mleq{}" right]\} ].
\mforall{}[eq:left:int\_term() {}\mrightarrow{} right:int\_term() {}\mrightarrow{} \{x:A| R[x;left "=" right]\} ].
\mforall{}[and:left:int\_formula()
{}\mrightarrow{} right:int\_formula()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left "\mwedge{}" right]\} ]. \mforall{}[or:left:int\_formula()
{}\mrightarrow{} right:int\_formula()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left "or" right]\} ].
\mforall{}[implies:left:int\_formula()
{}\mrightarrow{} right:int\_formula()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left "=>" right]\} ]. \mforall{}[not:form:int\_formula()
{}\mrightarrow{} \{x:A| R[x;form]\}
{}\mrightarrow{} \{x:A| R[x;"\mneg{}"form]\} ].
(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{} \{x:A| R[x;v]\} )
Date html generated:
2019_06_20-PM-00_46_31
Last ObjectModification:
2019_01_10-PM-09_15_19
Theory : omega
Home
Index