Nuprl Lemma : intlex-aux-reflexive

`∀[l1,l2:ℤ List].  intlex-aux(l1;l2) = tt supposing l1 = l2 ∈ (ℤ List)`

Proof

Definitions occuring in Statement :  intlex-aux: `intlex-aux(l1;l2)` list: `T List` btrue: `tt` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` so_apply: `x[s]` implies: `P `` Q` intlex-aux: `intlex-aux(l1;l2)` nil: `[]` it: `⋅` btrue: `tt` bool: `𝔹` all: `∀x:A. B[x]` cons: `[a / b]` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` less_than: `a < b` and: `P ∧ Q` less_than': `less_than'(a;b)` true: `True` squash: `↓T` not: `¬A` false: `False` prop: `ℙ` guard: `{T}` sq_type: `SQType(T)`
Lemmas referenced :  list_induction equal-wf-base bool_wf list_subtype_base int_subtype_base list_wf it_wf subtype_rel_union unit_wf2 spread_cons_lemma top_wf less_than_anti-reflexive less_than_wf subtype_base_sq and_wf equal_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation thin introduction extract_by_obid sqequalHypSubstitution isectElimination intEquality sqequalRule lambdaEquality hypothesis baseApply closedConclusion baseClosed hypothesisEquality applyEquality because_Cache independent_isectElimination independent_functionElimination inlEquality voidEquality voidElimination lambdaFormation rename dependent_functionElimination isect_memberEquality int_eqReduceTrueSq lessCases sqequalAxiom independent_pairFormation natural_numberEquality imageMemberEquality imageElimination productElimination axiomEquality equalityTransitivity equalitySymmetry hyp_replacement instantiate dependent_set_memberEquality applyLambdaEquality setElimination

Latex:
\mforall{}[l1,l2:\mBbbZ{}  List].    intlex-aux(l1;l2)  =  tt  supposing  l1  =  l2

Date html generated: 2017_09_29-PM-05_50_11
Last ObjectModification: 2017_07_26-PM-01_39_16

Theory : list_0

Home Index