[fmcmon]: https://fmc.imd.ufrn.br/
[aulabooks]: https://fmc.imd.ufrn.br/aulabook/
[fmcbook]: https://tsouanas.org/fmcbook

Desenvolvido pelo projeto [Monitoría FMCn][fmcmon].
Veja mais detalhes no site do projeto: fmc.imd.ufrn.br.
Veja também os outros [AulaBook™][aulabooks].
Referência principal: [fmcbook][fmcbook].

## 2023-08-17 (IM)

Vamos brincar de indução. Demonstre as seguintes:

- "A soma de Gauss" vale. Isto é, para todo natural $n$, $\sum\limits_{i=1}^{n}i = \dfrac{n(n+1)}{2}$;
- Todo inteiro maior ou igual à 8 pode ser escrito da forma 3x + 5y.

## ~~2023-08-18 (IG)~~
Demonstre a regra de "passar para o outro lado":
$$(\forall a, b, c : \text{Int})[a + b = c \iff a = c - b]$$

## 2023-08-22 (IM)

Indução. Nos naturais, definiremos as operações (+), (∙) e demonstraremos as seguintes:

- (+) é associativa
- (∙) é comutativa

## 2023-08-22 (DT)

Para todo $a, b, c \in \mathbb{Z}$, se $a\ |\ b$ e $a\ |\ c$ então $a\ |\ b + c$.
## 2023-08-22 (DT)

Seja $f: A \to A$ e $x \in A$, demonstre que um $x$ é um fixpoint da $f$ sse para todo $n \in \mathbb{N}$, $x$ é um fixpoint da $f^n$.

## 2023-08-24 (IM)

Introdução às relações.
Demonstre que a $(|) : Int \times Int \to Prop$ é uma pré-ordem.

## 2023-08-25 (IG)
Os inteiros e sua interface.

$\theta. \text{Unicidade dos inversos}$
$(\forall a, b : Int)[a+b = 0 \implies b = -a]$

## 2023-08-28 (DT)

Dada a definição recursiva  de $\alpha$, demonstre que para todo $x \in \mathbb{N}$ temos que $\alpha(1,x)=x+2$.

Definição de $\alpha$:

- [A1] $\ \ \alpha(0,x) = x+1$
- [A2] $\ \ \alpha(n+1,0) = \alpha(n,1)$
- [A3] $\ \ \alpha(n+1, x+1) = \alpha(n, \alpha(n+1,x))$

## 2023-08-29 (IM)

Relações. Seja $m : Int$. Demonstre que a $(≡_m) : Int \times Int \to Prop$ é uma relação de equivalência, isto é:

- $(≡_m)$ é reflexiva;
- $(≡_m)$ é transitiva; e
- $(≡_m)$ é simétrica.

Por fim, demonstre que $(≡_m)$ é uma congruência nos inteiros. Sejam $a, b : Int$.

- $(\forall x)[a + x ≡_m b + x]$ (garante (+))
- $(\forall x)[ax ≡_m bx]$ (garante (∙))
- $-a ≡_m -b$ (garante (-))

## 2023-08-29 (DT)
Demonstre que para todos $A, B, C$ conjuntos, se $A$ habitado e $A \subseteq B-C$ então $B\not\subseteq C$.

## 2023-08-30 (DT)
Seja $A$ um conjunto estruturado e $*$ uma operação binária e associativa no $A$, com identidade $u$. Demonstre que as seguintes definições de iterações são equivalentes:

Definição 1:

- $a^{*0} = u$ 
- $a^{*n+1} = a * a^{*n}$

Definição 2:

- $a_{*0} = u$
- $a_{*n+1} = a_{*n} * a$

Perceba contextos onde essa estrutura (associatividade e identidade da operação) é respeitada e portando as definições para iterações continuam equivalentes.

## 2023-09-01 (IG)
Trabalhando com a unicidade.
Definição de $\exists!$.

Seja $G$ um grupo (que raios é um grupo??), demonstre a unicidade do elemento neutro.
## 2023-09-05 (IM)

Funções. Sejam $n$ natural, e $f, g$ endomapas no $\mathbb{Z}$. Demonstre ou refute: $(f \circ g)^n = f^n \circ g^n$.

## 2023-09-05 (DT)
Demonstre que para todo natural $n$ temos $(F_{n+1},F_{n})=1$.
- Definição:
- $F_0 = 1$
- $F_1 = 1$
- $F_{n + 2} = F_{n + 1} + F_n$

## 2023-09-05 (DT)
Definimos a relação de ordem $\leq$ nos naturais pela:
- $n \leq m \iff (\exists k ∈ N)[ n + k = m ]$

a) Demonstre a seguinte proposição: $(\forall n,m)[n \leq Sm \iff n\leq m$ ou $n=Sm ].$

b) O que a $\leq$ precisa para ser considerada realmente uma ordem?

c) De que outra maneira poderia definir uma ordem nos naturais? Demonstre a "reflexividade da relação" para as duas definições propostas e compare as técnicas usadas para demonstrar em cada um dos casos.

## 2023-09-06 (DT)
Demonstre que para todos naturais $n, x, y$ temos que ${(n^x)}^y=n^{xy}$.

## 2023-09-11 (DT)

Seja $\to$ uma relação no conjunto $\mathbb N$ definida pela:

- $a \to b \iff a + 1 = b$

Demonstre que $(\forall a,b,n \in \mathbb N)[a \to^n b \implies a + n = b]$.

**Definições**:
- $x(R \diamond S)y \iff (\exists w)[x \mathrel R w \mathbin\& w \mathrel S y]$
- Definimos a relação $R^n$ recursivamente pelas:
- $R^0 = (=)$
- $R^{n + 1} = R \diamond R^n$

**Exercício extra**: Demonstre que para todo $n$ natural maior ou igual a $1$, temos $3^n-2$ ímpar.

## 2023-09-12 (DT)
(IRI)

A partir das definições recursivas de adição, multiplicação e exponenciação para os naturais, demonstre as seguintes proposições:

- $(\forall a, x, y: Nat)[a^{x+y} = a^{x}a^y]$
- $(\forall m: Nat)[m+0=0+m]$
- $(\forall a,b: Nat)[Sa+b=a+Sb]$
- $(\forall a,b: Nat)[a+b=b+a]$

## 2023-09-13 (DT)
(IDMa)

Partindo dos 3 axiomas mutiplicativos (associatividade, comutatividade, identidade), 4 axiomas aditivos (associatividade, comutatividade, identidade, inversos) e do axioma da distributividade, demonstre que as seguintes são equivalentes:
- $(\forall a, b: Int)[ab=0 \implies a=0 \ ou \ b=0 ]$
- $(\forall a, b, c: Int)[ca=cb \implies c=0 \ ou \ a=b]$

Mostre os lemmas necessários.

## 2023-09-18 (IG)
(IDMa)
Aritmética modular.
Definição congruência modular.
$\equiv_m$ é uma relação de equivalência.

## 2023-09-19 (DT)
Demonsre que a $\leq$ definida nos naturais é total.

## 2023-09-20 (DT)

- Defina a $length$ e a $concat$ para listas de Nats.
- Demonstre que para todas $l$, $l'$ listas de naturais, temos $length\ (concat \ l \ l')=length(l)+length(l')$.

## 2023-09-21 (IM)

Considere o $(A; ♡, κ)$ com a especificação seguinte, e demonstre que não tem como demonstrar a comutatividade de (♡), nem como refutá-la.

$(♡) : A × A → A$
$κ : A$
(Ass) : $(∀a,b,c)[ (a\ ♡\ b)\ ♡\ c = a\ ♡\ (b\ ♡\ c) ]$
(IdR) : $(∀a)[ a\ ♡\ κ = a ]$

*Dicas:*
- Modelo que satisfaz (♡)-comutatividade & modelo que não satisfaz (♡)-comutatividade;
- Seja econômico nos conjuntos, isto é, busque sempre os modelos com menos elementos possíveis;
- Em modelos maiores tente aproveitar um padrão na definição da (♡) com poucos elementos conhecidos.

## 2023-09-25 (IG)
Definição de M.D.C nos inteiros.
Vamos demonstrar que para quaisquer $a, b$ se $a$ divide $b$ então o mdc de $a$ e $b$ é o $a$.

O mdc de $a, b$ é igual ao mdc de $a, (a+b)$.

## 2023-09-26 (DT)

Demonstre que os subgrupos de $(Z; +)$ são fechados pelo mdc.

## 2023-09-27 (DT)
Demonstre que para todo $H ≤ (Z; +)$, existe $t \in Z$ tal que $H = tZ$.

## 2023-09-28 (IM)

Vamos 🎮︎? Baixe o [Lean 4](https://lean-lang.org/) e complete o jogo [ListNatGame](https://github.com/isaacmsl/ListNatGame).

## 2023-10-04 (DT)
- Defina nas listas as funções $length$, $append$, $reverse$.
- Demonstre que $length \ (reverse \ l) = length \ l$.

## 2023-10-09 (IG)

Inversos modulares.
$$(\forall m, a)[a \text{ possui inverso módulo } m \iff mdc(a, m) = 1]$$
<!-- Inversos modulares e o lemma de bezout -->

## 2023-10-09 (DT)
- Defina a $flaten$ para árvores.
- Demonstre que para toda árvore, a quantidade de folhas é sempre a quantidade de nodes mais 1.

## 2023-10-11 (DT)

Seja $\{A_n\}_n$ sequência de conjuntos e $\{D_n\}_n$ definida pelas:

- $D_0 = \emptyset$
- $D_{n+1} = D_n \cup A_n$

Demonstre que para todo $n$ natural $D_n \subseteq \bigcup_{m=0}^{\infty}A_m$.

## 2023-10-17 (DT)

- Demonstre que para todo $p$, $p$ irredutível sse $p$ primo.
- (Dica) Demonstre o seguinte lema: para todo $p$ irredutível e para todo $a$ inteiro. Se $p$ não divide $a$, então $(a,b)=1$

## 2023-10-17 (DT)

- Demonstre que $x$ irredutível sse $(\forall y)[y|x] \implies y=1 \ ou \ y=-1 \ ou \ y=x \ ou \ y=-x]$.
- Demonstre que para todos $p,q$ primos distintos, temos $(\forall n)[pq|n^2 \implies pq |n]$
- **Lema 1:** $(\forall a, b, d)[(d,a)=1 \ \ \& \ \ d|ab \implies d|b]$
- **Lema 2:** $(\forall a, b, m)[a|m \ \ \& \ \ b|m \ \ \& \ \ (a,b)=1 \implies ab|m]$

## 2023-10-19 (IM)

🎃 Matróides!

- Leia o artigo [Matróides e algoritmos gananciosos:
o que tem o c# a ver com as calças?](https://drive.google.com/file/d/1I7QdOlK8IH_Ko_GXrNVOF596G4OarIlq/view)
- Demonstre que o seguinte problema pode ser modelado como uma Matróide:
> Dadas *n* listas, encontrar uma lista com *n* elementos de tal forma que nenhum de seus elementos pertença a mesma posição em uma lista e que a soma dessa lista seja a menor possível.
- Descreva um algoritmo ganancioso que soluciona o problema acima.
- Veja os códigos desenvolvidos na aula [aqui](https://github.com/isaacmsl/matroids_and_greedy).

## 2023-10-20 (DT)

- Demonstre que: $(\forall n \geq 2)(\exists p$ primo $)[p|n]$
- Congruência módulo $m$:
- $(a,m)=1$ sse $a$ tem inverso módulo $m$.

## 2023-10-23 (IG)
- Funções multiplicativas e suas propriedades

Seja $f: \mathbb{Z} \to \mathbb{Z}$, dizemos que $f$ é **multiplicativa** sse para quaisquer $p, q$ co-primos
$f(pq) = f(p)f(q)$

## 2023-10-24 (DT)
- Seja $x$ inteiro. Demonstre que $(\forall y)[x \equiv y \ (mod \ 0) \implies (\forall m \geq 0)[x \equiv y \ (mod \ m)]]$
- Cancelamento módulo $m$.
- Partindo de umas ideias de **Euler**..
- Demonstre que $(\forall n \geq 3)[2|\phi (n)]$. *(Parte 1)*

## 2023-10-25 (DT)
- Partindo de umas ideias de **Euler**..
- Demonstre que $(\forall n \geq 3)[2|\phi (n)]$. *(Parte 2)*
- Sejam $e,d,n$ inteiros tq $e,\phi(n)$ coprimos e $d$ inverso de $e$ módulo $\phi (n)$. Demonstre que $(\forall m)[(m,n)=1 \implies (m^e)^d \equiv m \ (mod \ m)]$.

## 2023-10-27 (DT)
🌳 IRI
- Defina o tipo árvore binária com informações apenas nas pontas.
- Defina as *size*, *depth* que retornam, respectivamente, as quantidade de pontas e a profundidade para árvores binárias.
- Demonstre que para toda árvore binária finita $t$, $size \ t \leq 2^{depth \ t}$.

## 2023-11-01 (DT)
Demonstre as leis de Functor para List.

## 2023-11-03 (DT)
Demonstre que para todo conjunto $A$ finito habitado e toda função total $f:A\to A$, $f$ injetiva sse $f$ sobrejetiva. *(Parte 1)*

## 2023-11-08 (DT)
Demonstre que para todos $a,b$ inteiros positivos, temos $(2^a-1,2^b-1)=2^{(a,b)}-1$.

Dica: demonstre o lema $(\forall n:\mathbb{N})(\forall a:\mathbb{Z})[a-1|a^k-1]$

<!-- ## 2023-11-07 (DT)*
Demonstre que para todo conjunto $A$ finito habitado e toda função total $f:A\to A$, $f$ injetiva sse $f$ sobrejetiva. *(Parte 2)* -->

## 2023-11-10 (DT)
Demonstre que para todo conjunto $A \subseteq \mathbb{N}$, se $A$ infinito então $|A|=| \mathbb{N} |$.

## 2023-11-15 (IM)

Demonstre que as sequências $(1 + 10^{-n})_n$, $(1 - 10^{-n})_n$ convergem no mesmo valor. Qual(is) conclusão(ões) podemos tomar a partir disso?