Step
*
of Lemma
compose-flips_wf
∀k:ℕ. ∀flips:(ℕk × ℕk) List. (compose-flips(flips) ∈ ℕk ⟶ ℕk)
BY
{ (Auto THEN Unfold `compose-flips` 0 THEN GenConclAtAddrType ⌜(ℕk ⟶ ℕk) List⌝ [2;3]⋅ THEN Auto) }
Latex:
Latex:
\mforall{}k:\mBbbN{}. \mforall{}flips:(\mBbbN{}k \mtimes{} \mBbbN{}k) List. (compose-flips(flips) \mmember{} \mBbbN{}k {}\mrightarrow{} \mBbbN{}k)
By
Latex:
(Auto THEN Unfold `compose-flips` 0 THEN GenConclAtAddrType \mkleeneopen{}(\mBbbN{}k {}\mrightarrow{} \mBbbN{}k) List\mkleeneclose{} [2;3]\mcdot{} THEN Auto)
Home
Index