Przemebra/praca-magisterska/agda-tex/przyklad-liczby-calkowite.tex

\>[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]\<%