726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskilogic DFOL

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elknerspec Matrices =

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiNat :: Sort

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill MossakowskiMat :: Nat -> Nat -> Sort

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskiplus :: Pi m, n : Nat. Mat(m, n) -> Mat(m, n) -> Mat(m, n)

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowskimult :: Pi p, q, r : Nat. Mat(p, q) -> Mat(q, r) -> Mat(p, r)

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski.forall m, n : Nat; A, B : Mat(m, n). plus(m, n, A, B) == plus(m, n, B, A) %(plus_commut)%

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski.forall m, n : Nat; A, B, C : Mat(m, n). plus(m, n, plus(m, n, A, B), C) == plus(m, n, A, plus(m, n, B, C)) %(plus_assoc)%

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski.forall p, q, r, s : Nat; A : Mat(p, q); B : Mat(q, r); C : Mat(r, s). mult(p, r, s, mult(p, q, r, A, B), C) == mult(p, q, s, A, mult(q, r, s, B, C)) %(mult_assoc)%

726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski