---

Step * of Lemma ml-reduce-sq

∀[A,B:Type].
  (∀[f:A ⟶ B ⟶ B]. ∀[l:A List]. ∀[b:B].  (ml-reduce(f;b;l) ~ reduce(f;b;l))) supposing 
     ((valueall-type(A) ∧ A) and 
     valueall-type(B))
BY
{ (InductionOnList
   THEN Intro
   THEN All (RepUR ``ml-reduce spreadcons ml_apply``)
   THEN RW (AddrC [1] (SweepUpC UnrollRecursionC)) 0
   THEN Reduce 0
   THEN (Assert value-type(B ⟶ B) BY
               (Auto THEN D 0 THEN D 0 With ⌜b⌝  THEN EAuto 1))
   THEN (Assert valueall-type(A ⟶ B ⟶ B) BY
               Auto)
   THEN (CallByValueReduceOn ⌜f⌝ 0⋅ THENA Auto)
   THEN ((CallByValueReduce 0 THENA Auto) THENM Reduce 0)
   THEN (Trivial
   ORELSE (((CallByValueReduce 0 THENA Auto) THENM Reduce 0)
           THEN (CallByValueReduceOn ⌜f⌝ 8⋅ THENA Auto)
           THEN (RWO "8" 0 THENA Auto))
   )) }

1
1. A : Type
2. B : Type
3. valueall-type(B)
4. valueall-type(A) ∧ A
5. f : A ⟶ B ⟶ B
6. u : A
7. v : A List
8. ∀[b:B]
     (let y ⟵ v
      in let y ⟵ b
         in fix((λreduce,f,b,l. if null(l)
                               then b
                               else let a,as = l 
                                    in let y ⟵ let y ⟵ as
                                                in let y ⟵ b in let y ⟵ f in reduce y y y
                                       in let y ⟵ a in f y y
                               fi )) 
            f 
            y 
         y ~ reduce(f;b;v))
9. [b] : B
10. value-type(B ⟶ B)
11. valueall-type(A ⟶ B ⟶ B)
⊢ let y@0 ⟵ reduce(f;b;v)
  in let y@0 ⟵ u in f y@0 y@0 ~ f u reduce(f;b;v)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    (\mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[l:A  List].  \mforall{}[b:B].    (ml-reduce(f;b;l)  \msim{}  reduce(f;b;l)))  supposing 
          ((valueall-type(A)  \mwedge{}  A)  and 
          valueall-type(B))


By

---

Latex:
(InductionOnList
  THEN  Intro
  THEN  All  (RepUR  ``ml-reduce  spreadcons  ml\_apply``)
  THEN  RW  (AddrC  [1]  (SweepUpC  UnrollRecursionC))  0
  THEN  Reduce  0
  THEN  (Assert  value-type(B  {}\mrightarrow{}  B)  BY
                          (Auto  THEN  D  0  THEN  D  0  With  \mkleeneopen{}b\mkleeneclose{}    THEN  EAuto  1))
  THEN  (Assert  valueall-type(A  {}\mrightarrow{}  B  {}\mrightarrow{}  B)  BY
                          Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}f\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  ((CallByValueReduce  0  THENA  Auto)  THENM  Reduce  0)
  THEN  (Trivial
  ORELSE  (((CallByValueReduce  0  THENA  Auto)  THENM  Reduce  0)
                  THEN  (CallByValueReduceOn  \mkleeneopen{}f\mkleeneclose{}  8\mcdot{}  THENA  Auto)
                  THEN  (RWO  "8"  0  THENA  Auto))
  ))

---

Home Index