Nuprl Lemma : flip_twice

`∀[k:ℤ]. ∀[x,y,i:ℕk].  (((y, x) ((y, x) i)) = i ∈ ℤ)`

Proof

Definitions occuring in Statement :  flip: `(i, j)` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` apply: `f a` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` compose: `f o g` int_seg: `{i..j-}` true: `True` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  int_seg_wf equal_wf squash_wf true_wf flip_inverse subtype_rel_self iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut hypothesis Error :inhabitedIsType,  hypothesisEquality sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin axiomEquality extract_by_obid natural_numberEquality because_Cache Error :universeIsType,  intEquality setElimination rename applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed instantiate independent_isectElimination productElimination independent_functionElimination

Latex:
\mforall{}[k:\mBbbZ{}].  \mforall{}[x,y,i:\mBbbN{}k].    (((y,  x)  ((y,  x)  i))  =  i)

Date html generated: 2019_06_20-PM-01_36_14
Last ObjectModification: 2018_09_26-PM-05_52_32

Theory : list_1

Home Index