Nuprl Lemma : map_swap

`∀[A,B:Type]. ∀[f:B ⟶ A]. ∀[x:B List]. ∀[i,j:ℕ||x||].  (map(f;swap(x;i;j)) = swap(map(f;x);i;j) ∈ (A List))`

Proof

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

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:B  {}\mrightarrow{}  A].  \mforall{}[x:B  List].  \mforall{}[i,j:\mBbbN{}||x||].    (map(f;swap(x;i;j))  =  swap(map(f;x);i;j))

Date html generated: 2016_05_15-PM-02_05_06
Last ObjectModification: 2015_12_27-AM-00_22_00

Theory : list!

Home Index