### Nuprl Lemma : flip_wf

`∀[k:ℕ]. ∀[i,j:ℕk].  ((i, j) ∈ ℕk ⟶ ℕk)`

Proof

Definitions occuring in Statement :  flip: `(i, j)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` flip: `(i, j)` int_seg: `{i..j-}` nat: `ℕ`
Lemmas referenced :  ifthenelse_wf eq_int_wf int_seg_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis natural_numberEquality because_Cache axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  isect_memberEquality Error :universeIsType

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[i,j:\mBbbN{}k].    ((i,  j)  \mmember{}  \mBbbN{}k  {}\mrightarrow{}  \mBbbN{}k)

Date html generated: 2019_06_20-PM-01_35_41
Last ObjectModification: 2018_09_26-PM-05_51_11

Theory : list_1

Home Index