### Nuprl Lemma : swap_length

`∀[T:Type]. ∀[L:T List]. ∀[i,j:ℕ||L||].  (||swap(L;i;j)|| = ||L|| ∈ ℤ)`

Proof

Definitions occuring in Statement :  swap: `swap(L;i;j)` length: `||as||` list: `T List` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  swap: `swap(L;i;j)` uall: `∀[x:A]. B[x]` member: `t ∈ T` top: `Top`
Lemmas referenced :  permute_list_length length_wf int_seg_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality isect_memberEquality voidElimination voidEquality hypothesis natural_numberEquality axiomEquality because_Cache

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[i,j:\mBbbN{}||L||].    (||swap(L;i;j)||  =  ||L||)

Date html generated: 2016_05_15-PM-02_04_13
Last ObjectModification: 2015_12_27-AM-00_22_12

Theory : list!

Home Index