Nuprl Lemma : sqeq-copath5

[n,m:Top].  ((m 1) 1)


Proof




Definitions occuring in Statement :  uall: [x:A]. B[x] top: Top subtract: m add: m natural_number: $n sqequal: t
Definitions unfolded in proof :  not: ¬A is-exception: is-exception(t) false: False implies:  Q prop: top: Top subtype_rel: A ⊆B uiff: uiff(P;Q) uimplies: supposing a and: P ∧ Q has-value: (a)↓ subtract: m member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  exception-not-bottom bottom_diverge exception-not-value_1 int_subtype_base sqle_wf_base minus-minus minus-add zero-add add-commutes minus-one-mul-top add-swap minus-one-mul base_wf add-associates add-is-int-iff minus-is-int-iff int-value-type value-type-has-value top_wf is-exception_wf has-value_wf_base
Rules used in proof :  exceptionAdd minusExceptionCases sqleRule independent_functionElimination exceptionSqequal axiomSqleEquality addExceptionCases applyLambdaEquality hyp_replacement sqleReflexivity natural_numberEquality minusEquality voidEquality voidElimination lambdaEquality applyEquality addEquality callbyvalueMinus equalitySymmetry equalityTransitivity independent_isectElimination intEquality productElimination callbyvalueAdd because_Cache isect_memberEquality sqequalAxiom hypothesis hypothesisEquality baseClosed closedConclusion baseApply isectElimination sqequalHypSubstitution extract_by_obid divergentSqle sqequalSqle thin sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[n,m:Top].    ((m  +  1)  -  n  -  1  \msim{}  m  -  n  -  1  -  1)



Date html generated: 2016_12_12-AM-09_16_29
Last ObjectModification: 2016_12_11-PM-05_22_46

Theory : co-recursion


Home Index