Aaron W. Hsu arcfide

## keybase.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                arcfide
                / keybase.md
            
            
              Created
              March 27, 2015 00:58
            
          
    Keybase proof

I hereby claim:

I am arcfide on github.
I am arcfide (https://keybase.io/arcfide) on keybase.
I have a public key whose fingerprint is 0DA1 939E 7315 805B 4514  9D23 EBEF 63A2 B6C0 03AD

To claim this, I am signing this object:

  
## fract_rep_apl
{⎕FR←1287 ⋄ (B=⊃⌽{(1|d)((⊃⌽⍵),⌊d←2×⊃⍵)}⍣64⊢(¯1+⍵*.5) ⍬)}2

## gist:3814120
definition sv2vl :: "nat ⇒ 'a list ⇒ 'a list" where
  "sv2vl n ls ≡
     if ls = []
     then (replicate n fill)
     else take n (concat (replicate (1 + n div length ls) ls))"

lemma sv2vl_mod [simp]:
  "i < n ∧ ls ≠ [] ⟹ sv2vl n ls ! i = ls ! (i mod length ls)"
by ???
	definition sv2vl :: "nat ⇒ 'a list ⇒ 'a list" where
	"sv2vl n ls ≡
	if ls = []
	then (replicate n fill)
	else take n (concat (replicate (1 + n div length ls) ls))"

	lemma sv2vl_mod [simp]:
	"i < n ∧ ls ≠ [] ⟹ sv2vl n ls ! i = ls ! (i mod length ls)"
	by ???