Commit 6237918b by Sven Wille

### a bit of finseqs

parent 615d2dcf
 ... ... @@ -7,19 +7,19 @@ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory FinSequences : base:?Logic = include arith:?NaturalArithmetics ❙ below : ℕ ⟶ type ❘ = [n] ⟨ x : ℕ | ⊦ x < n ⟩ ❙ toBelow : {n : ℕ} below (Succ n) ❘# toB 1❙ succBelow : {n : ℕ} below n ⟶ below (Succ n) ❘# succB 2❙ // toBelow : {n : ℕ} below (Succ n) ❘# toB 1❙ // succBelow : {n : ℕ} below n ⟶ below (Succ n) ❘# succB 2❙ belowIsSubtypeOfNat : {n : ℕ} (below n) <* ℕ ❙ // belowIsSubtypeOfNat : {n : ℕ} (below n) <* ℕ ❙ belowToNat : {n : ℕ} below (Succ n) ⟶ ℕ ❘# btn 1 2❙ belowToNatBaseCase : {m : ℕ} ⊦ belowToNat m (toBelow m) ≐ m❙ belowToNatRecCase : {m : ℕ, b : below (Succ m)} ⊦ belowToNat (Succ m) (succBelow (Succ m) b) ≐ belowToNat m b ❙ // belowToNat : {n : ℕ} below (Succ n) ⟶ ℕ ❘# btn 1 2❙ // belowToNatBaseCase : {m : ℕ} ⊦ belowToNat m (toBelow m) ≐ m❙ // belowToNatRecCase : {m : ℕ, b : below (Succ m)} ⊦ belowToNat (Succ m) (succBelow (Succ m) b) ≐ belowToNat m b ❙ belowToNatExample : ⊦ btn 3 (toB 3) ≐ 3❙ belowToNatExample2 : ⊦ btn 4 (succB (toB 3)) ≐ 3 ❙ belwoToNatExample2_2 : ⊦ belowToNat (Succ 3) (succBelow (Succ 3) (toBelow 3)) ≐ 3❙ // belowToNatExample : ⊦ btn 3 (toB 3) ≐ 3❙ // belowToNatExample2 : ⊦ btn 4 (succB (toB 3)) ≐ 3 ❙ // belwoToNatExample2_2 : ⊦ belowToNat (Succ 3) (succBelow (Succ 3) (toBelow 3)) ≐ 3❙ // belowToNat2 : {n : ℕ} below (Succ n) ⟶ ℕ ❘= [n, b] n ❘# btn2 %I1 ❙ // belowToNat3 : {n : ℕ, m : ℕ} below n ⟶ ⊦ m < n ⟶ ℕ ❘= [n , m , b, p ] m ❘# btn3 %I1 ❙ ... ... @@ -31,11 +31,11 @@ theory FinSequences : base:?Logic = nonEmptyFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n, A , f] 0 < n ❘# nefs %I1 %I2 ❙ disjointFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool❙ disjointFinSeq_prop_trivial : {A : type,f : finSeq 0 A} ⊦ disjointFinSeq_prop 0 A f ≐ true❙ disjointFinSeq_prop_step // : {A : type , n : ℕ , f : disjointFinSeq_prop : {n : ℕ, A : type} finSeq n A ⟶ bool ❘= [n,A,fs] ∀[x] ∀[y] y ≐ x ∨ fs x ≠ fs y❙ // disjointFinSeq_prop_trivial : {A : type,f : finSeq 0 A} ⊦ disjointFinSeq_prop 0 A f ≐ true❙ // disjointFinSeq_prop_step // : {A : type , n : ℕ , f : finSeq (succ n) A} ⊦ disjointFinSeq_prop (succ n) A f ≐ ∀ [m1 : below (succ n)] ∀ [m2 : below (succ n)] ⊦ m1 ≠ m2 ⟶ ⊦ true ❙ belowShift : {n : ℕ , m : ℕ} below n ⟶ below (n + m)❙ // belowShift : {n : ℕ , m : ℕ} below n ⟶ below (n + m)❙ // belowShift_base : {n, b} ⊦ belowShift n 0 b ≐ b❙ // finSeqSum : {n : ℕ , b : below n} ❙ ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!