Require Import ZArith.

Check 0%Z.

(************Drzewa binarne ***************)


Inductive btree : Set :=
  leaf : btree
| node : Z -> btree -> btree -> btree.

(* Zdefiniuj:

Definition right_son (t:btree) : btree :=

Fixpoint zero_present (t:btree) : bool :=

Fixpoint sum_all_values (t:btree) : Z :=
*)

Inductive fbtree : Set :=
  fleaf : fbtree
| fnode : Z -> (bool -> fbtree) -> fbtree.

(*Zdefiniuj:
 
Definition fright_son (t:fbtree) : btree :=

Fixpoint fzero_present (t:fbtree) : bool :=

Fixpoint fsum_all_values (t:fbtree) : Z :=
*)

(*Zdefiniuj bijekcje pomiędzy btree i fbtree *)
 
Fixpoint f1 (t: btree){struct t} : fbtree := 

Fixpoint f2 (t: fbtree){struct t} : btree := 

Lemma id1: forall (t:btree), f2 (f1 t) = t.
 
(*Czego brakuje by udowodnic poniższy lemat*)

Lemma id2: forall (t:fbtree), f1 (f2 t) = t.


(************** Drzewa o nieskończonym rozgałęzieniu **********)

Inductive inf_br_tree : Set :=
  inf_br_leaf : inf_br_tree
| inf_br_node : Z -> (nat -> inf_br_tree) -> inf_br_tree.

(*Napisz funkcje sprawdzającą czy jest w drzewie ograniczonym do 
n+1 pierwszych poddrzew w każdym wierzchołku występuje zero
*)

Fixpoint inf_br_zero_present (n:nat)(t:inf_brtree){struct t} : bool :=

(*
Napisz funkcje sumujacą wartości w drzewie ograniczonym do n+1 
poddrzew w każdym wierzchołku

Rada: 
wcześniej napisz funkcję sum (n:nat)(f:nat ->Z):Z która oblicza sumę 
f(0) + f(1) +... f(n)
*)

Fixpoint n_sum_all_values (n:nat)(t:inf_br_tree){struct t} : Z :=