Step * 1 1 1 1 of Lemma permutation-sv-list


1. Type
2. L1 List
3. L2 List
4. single-valued-list(L1;A)@i
5. : ℕ||L1|| ─→ ℕ||L1||@i
6. Inj(ℕ||L1||;ℕ||L1||;f)@i
7. L2 (L1 f) ∈ (A List)@i
⊢ ||L1|| ||(L1 f)|| ∈ ℤ
BY
(InstLemma `permute_list_length` [⌈A⌉;⌈L1⌉;⌈f⌉]⋅ THEN Auto) }


Latex:



Latex:

1.  A  :  Type
2.  L1  :  A  List
3.  L2  :  A  List
4.  single-valued-list(L1;A)@i
5.  f  :  \mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L1||@i
6.  Inj(\mBbbN{}||L1||;\mBbbN{}||L1||;f)@i
7.  L2  =  (L1  o  f)@i
\mvdash{}  ||L1||  =  ||(L1  o  f)||


By


Latex:
(InstLemma  `permute\_list\_length`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}L1\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)




Home Index