### Nuprl Lemma : mccarthy91-sqeq

`∀x:Top. (mccarthy91(x) ~ if (x) < (102)  then 91  else (x - 10))`

Proof

Definitions occuring in Statement :  mccarthy91: `mccarthy91(x)` top: `Top` all: `∀x:A. B[x]` less: `if (a) < (b)  then c  else d` subtract: `n - m` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` squash: `↓T` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` less_than: `a < b` less_than': `less_than'(a;b)` top: `Top` true: `True` not: `¬A` false: `False` prop: `ℙ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` satisfiable_int_formula: `satisfiable_int_formula(fmla)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` mccarthy91: `mccarthy91(x)` has-value: `(a)↓`
Lemmas referenced :  mccarthy91_wf1 le_int_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf eqff_to_assert equal_wf bool_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot full-omega-unsat intformand_wf intformle_wf itermVar_wf itermConstant_wf intformnot_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_formula_prop_wf assert_wf bnot_wf not_wf le_wf bool_cases assert_of_le_int iff_transitivity iff_weakening_uiff assert_of_bnot sqle_wf_base squash_wf true_wf base_wf int_subtype_base subtype_rel_self iff_weakening_equal has-value_wf_base is-exception_wf exception-not-value value-type-has-value int-value-type
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis intEquality isectElimination natural_numberEquality because_Cache equalityTransitivity equalitySymmetry applyLambdaEquality setElimination rename sqequalRule imageMemberEquality baseClosed imageElimination unionElimination equalityElimination productElimination independent_isectElimination lessCases isect_memberFormation axiomSqEquality isect_memberEquality independent_pairFormation voidElimination voidEquality independent_functionElimination dependent_pairFormation promote_hyp instantiate cumulativity approximateComputation lambdaEquality int_eqEquality impliesFunctionality sqequalSqle sqleRule divergentSqle applyEquality baseApply closedConclusion universeEquality sqleReflexivity lessExceptionCases axiomSqleEquality exceptionSqequal callbyvalueLess

Latex:
\mforall{}x:Top.  (mccarthy91(x)  \msim{}  if  (x)  <  (102)    then  91    else  (x  -  10))

Date html generated: 2019_06_20-PM-01_19_03
Last ObjectModification: 2018_08_20-PM-09_31_07

Theory : int_2

Home Index