Nuprl Lemma : bdd-all-btrue

[n:ℕ]. (bdd-all(n;x.tt) tt)


Proof




Definitions occuring in Statement :  bdd-all: bdd-all(n;i.P[i]) nat: btrue: tt uall: [x:A]. B[x] sqequal: t
Definitions unfolded in proof :  bdd-all: bdd-all(n;i.P[i]) uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  guard: {T} uimplies: supposing a prop: all: x:A. B[x] top: Top decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q uiff: uiff(P;Q) subtract: m subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) true: True band: p ∧b q ifthenelse: if then else fi  btrue: tt bool: 𝔹 unit: Unit it: bfalse: ff exists: x:A. B[x] sq_type: SQType(T) bnot: ¬bb assert: b
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf primrec0_lemma istype-void decidable__le subtract_wf istype-false not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel primrec-unroll lt_int_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination Error :lambdaFormation_alt,  natural_numberEquality independent_isectElimination independent_functionElimination voidElimination Error :universeIsType,  Error :lambdaEquality_alt,  dependent_functionElimination axiomSqEquality Error :isect_memberEquality_alt,  unionElimination independent_pairFormation productElimination addEquality applyEquality intEquality minusEquality Error :inhabitedIsType,  equalityTransitivity equalitySymmetry because_Cache equalityElimination Error :dependent_pairFormation_alt,  Error :equalityIsType1,  promote_hyp instantiate cumulativity

Latex:
\mforall{}[n:\mBbbN{}].  (bdd-all(n;x.tt)  \msim{}  tt)



Date html generated: 2019_06_20-PM-01_04_56
Last ObjectModification: 2019_06_20-PM-01_00_25

Theory : bool_1


Home Index