Commit 61a54382 authored by Sven Wille's avatar Sven Wille

finsequences foldr error

parent 2ed06e52
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:5504.158.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#108.4.0:128.4.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#409.15.0:433.15.24"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#3825.92.0:3855.92.30"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?INatArith]" target="http://mathhub.info/MitM/smglom/arithmetics?INatArith"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4134.108.0:4149.108.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?Between]" target="http://mathhub.info/MitM/smglom/arithmetics?Between"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4743.137.0:4756.137.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NatConversions]" target="http://mathhub.info/MitM/smglom/arithmetics?NatConversions"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#5236.149.0:5256.149.20"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#0.0.0:5764.167.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/MitM/smglom/arithmetics"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#108.4.0:128.4.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics]" target="http://mathhub.info/MitM/smglom/arithmetics?NaturalArithmetics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#409.15.0:433.15.24"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers]" target="http://mathhub.info/MitM/smglom/arithmetics?InductiveNaturalNumbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#3825.92.0:3855.92.30"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?INatArith]" target="http://mathhub.info/MitM/smglom/arithmetics?INatArith"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4134.108.0:4149.108.15"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?Between]" target="http://mathhub.info/MitM/smglom/arithmetics?Between"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#4743.137.0:4756.137.13"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?NatConversions]" target="http://mathhub.info/MitM/smglom/arithmetics?NatConversions"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#5236.149.0:5256.149.20"/></metadata></mref><mref name="[http://mathhub.info/MitM/smglom/arithmetics?INatProps]" target="http://mathhub.info/MitM/smglom/arithmetics?INatProps"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/MitM/smglom/arithmetics/naturals.mmt#5508.161.0:5523.161.15"/></metadata></mref></omdoc>
\ No newline at end of file
......@@ -5,3 +5,4 @@ Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathh
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?INatArith
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?Between
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?NatConversions
Declares http://mathhub.info/MitM/smglom/arithmetics/naturals.omdoc http://mathhub.info/MitM/smglom/arithmetics?INatProps
......@@ -163,6 +163,7 @@ theory INatProps : base:?Logic =
include ?INatArith ❙
lemma_Zero_lt_Suc : {m : INat} ⊦ ltN Zero (Suc m) ❙
lemma_Zero_le_Suc : {m : INat} ⊦ leN Zero (Suc m) ❙
lemma_One_le_Suc : {m : INat} ⊦ ltN (Suc Zero) (Suc m) ❙
lemma_One_le_Suc : {m : INat} ⊦ leN (Suc Zero) (Suc m) ❙
// lemma_le_Suc_le ❙
......@@ -31,20 +31,22 @@ theory FinSeqProps : base:?InductiveTypes =
theory FinSeqFunctions : base:?Logic =
theory FinSeqFunctions : base:?InductiveTypes =
include ?FinSequences ❙
include arith:?INatProps❙
finiteSequenceMap : {A : type} {B : type} {n : INat} finSeq n A ⟶ (A ⟶ B) ⟶ finSeq n B ❘= [A , B , n , fn , mp] [a ,b ,c] mp (fn a b c) ❘ # finSeqMap 4 5 ❙
def finiteSequenceFoldL : (A : type , B : type , fn : A ⟶ B ⟶ A , starValue : A, n : INat ) ❘ =
finSeqFoldR : {m : INat } ⊦ leN m n ⟶ finSeq n B ⟶ A❙
Zero = [h][fs] startValue ❙
Suc = [m][h][fs] fs (Suc m) (lemma_one_le_Suc (Suc m)) h finSeqFoldR m fs❙
def finiteSequenceFoldR (A : type , B : type , fn : A ⟶ B ⟶ B ) ❘ =
finSeqFoldR : {n : INat }{m : INat } B ⟶ ⊦ leN n m ⟶ finSeq n A ⟶ B ❙
// Zero = [A : type][B : type][n : INat][startValue : B][p : ⊦ leN Zero n][fs : finSeq n A][fn : A ⟶ B ⟶ B] startValue ❙
// Suc = [m : INat][A : type][B : type][n : INat][startValue : B][p : ⊦ leN Zero n][fs : finSeq n A][fn : A ⟶ B ⟶ B] startValue ❙
// Suc = [m][A][B][n][startValue][h][fs][fn] fn (fs (Suc m) (lemma_One_le_Suc m) h) startValue ❙
// bla : {A : type} {n : INat} {m : INat} ⊦ leN (Suc Zero ) m ⟶ ⊦ leN m n ⟶ finSeq n A ⟶ A ❘ = [A , n , m , p , p0 , fs] fs m p p0 ❙
theory FinSeqProd : base:?Logic =
finSeqIntervalProd : ❙
// finSeqIntervalProd : ❙
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment