Nuprl Lemma : intformeq-right_wf

[v:int_formula()]. intformeq-right(v) ∈ int_term() supposing ↑intformeq?(v)


Proof




Definitions occuring in Statement :  intformeq-right: intformeq-right(v) intformeq?: intformeq?(v) int_formula: int_formula() int_term: int_term() assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) sq_type: SQType(T) guard: {T} eq_atom: =a y ifthenelse: if then else fi  intformeq?: intformeq?(v) pi1: fst(t) assert: b bfalse: ff false: False exists: x:A. B[x] prop: or: P ∨ Q bnot: ¬bb intformeq-right: intformeq-right(v) pi2: snd(t)
Lemmas referenced :  int_formula-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom assert_wf intformeq?_wf int_formula_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid promote_hyp sqequalHypSubstitution productElimination thin hypothesis_subsumption hypothesis hypothesisEquality applyEquality sqequalRule isectElimination tokenEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination instantiate cumulativity atomEquality dependent_functionElimination independent_functionElimination because_Cache voidElimination dependent_pairFormation

Latex:
\mforall{}[v:int\_formula()].  intformeq-right(v)  \mmember{}  int\_term()  supposing  \muparrow{}intformeq?(v)



Date html generated: 2017_04_14-AM-09_00_56
Last ObjectModification: 2017_02_27-PM-03_43_02

Theory : omega


Home Index