123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100 |
- \>[0]\AgdaFunction{twierdzenie}\AgdaSpace{}
- \AgdaSymbol{:}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaBound{a}\AgdaSpace{}
- \AgdaSymbol{:}\AgdaSpace{}
- \AgdaDatatype{ℤ}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaSymbol{→}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaBound{b}\AgdaSpace{}
- \AgdaSymbol{:}\AgdaSpace{}
- \AgdaDatatype{ℤ}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaSymbol{→}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaBound{założenie}\AgdaSpace{}
- \AgdaSymbol{:}\AgdaSpace{}
- \AgdaBound{a}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{{-}}}\AgdaSpace{}
- \AgdaBound{b}\AgdaSpace{}
- \AgdaOperator{\AgdaDatatype{≡}}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaOperator{\AgdaInductiveConstructor{+}}\AgdaSpace{}
- \AgdaNumber{0}\AgdaSymbol{))}\AgdaSpace{}
- \AgdaSymbol{→}\AgdaSpace{}
- \AgdaBound{a}\AgdaSpace{}
- \AgdaOperator{\AgdaDatatype{≡}}\AgdaSpace{}
- \AgdaBound{b}\<
- \\
- \>[0]\AgdaFunction{twierdzenie}\AgdaSpace{}
- \AgdaBound{a}\AgdaSpace{}
- \AgdaBound{b}\AgdaSpace{}
- \AgdaBound{założenie}\AgdaSpace{}
- \AgdaSymbol{=}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{begin}}\<
- \\
- \>[0][@{}l@{\AgdaIndent{0}}]
- \>[2]\AgdaBound{a}
- \>[16]\AgdaOperator{\AgdaFunction{≡⟨}}\AgdaSpace{}
- \AgdaFunction{sym}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaFunction{+{-}identity$^r$}\AgdaSpace{}
- \AgdaBound{a}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{⟩}}\<
- \\
- \>[2]\AgdaBound{a}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{+}}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaOperator{\AgdaInductiveConstructor{+}}\AgdaSpace{}
- \AgdaNumber{0}\AgdaSymbol{)}
- \>[16]\AgdaOperator{\AgdaFunction{≡⟨}}\AgdaSpace{}
- \AgdaFunction{cong₂}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaInductiveConstructor{refl}\AgdaSpace{}
- \AgdaSymbol{\{}\AgdaArgument{x}\AgdaSpace{}
- \AgdaSymbol{=}\AgdaSpace{}
- \AgdaBound{a}\AgdaSymbol{\})}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaFunction{sym}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaFunction{+{-}inverse$^l$}\AgdaSpace{}
- \AgdaBound{b}\AgdaSymbol{))}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{⟩}}\<
- \\
- \>[2]\AgdaBound{a}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{+}}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaOperator{\AgdaFunction{{-}}}\AgdaSpace{}
- \AgdaBound{b}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{+}}\AgdaSpace{}
- \AgdaBound{b}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{≡⟨}}\AgdaSpace{}
- \AgdaFunction{sym}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaFunction{+{-}assoc}\AgdaSpace{}
- \AgdaBound{a}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaOperator{\AgdaFunction{{-}}}\AgdaSpace{}
- \AgdaBound{b}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaBound{b}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{⟩}}\<
- \\
- \>[2]\AgdaSymbol{(}\AgdaBound{a}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{{-}}}\AgdaSpace{}
- \AgdaBound{b}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{+}}\AgdaSpace{}
- \AgdaBound{b}
- \>[16]\AgdaOperator{\AgdaFunction{≡⟨}}\AgdaSpace{}
- \AgdaFunction{cong₂}\AgdaSpace{}
- \AgdaSymbol{(}\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}+\AgdaUnderscore{}}}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaBound{założenie}\AgdaSpace{}
- \AgdaInductiveConstructor{refl}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{⟩}}\<
- \\
- \>[2]\AgdaSymbol{(}\AgdaOperator{\AgdaInductiveConstructor{+}}\AgdaSpace{}
- \AgdaNumber{0}\AgdaSymbol{)}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{+}}\AgdaSpace{}
- \AgdaBound{b}
- \>[16]\AgdaOperator{\AgdaFunction{≡⟨}}\AgdaSpace{}
- \AgdaFunction{+{-}identity$^l$}\AgdaSpace{}
- \AgdaBound{b}\AgdaSpace{}
- \AgdaOperator{\AgdaFunction{⟩}}\<
- \\
- \>[2]\AgdaBound{b}
- \>[16]\AgdaOperator{\AgdaFunction{$\qed$}}\<
- \\
- \>[0]\<
|