Example proofs demonstrating Armstrong ’s axiom system for FD:

FD1 Reflexivity

FD2 Augmentation

FD3 Transitivity

FD4 Union

FD5 Decomposition

FD6 Psuedo transitivity

FD1 Reflexivity: if Y Í X Í R, then F |- X → Y.

{branch-name} Í {branch-name, assets} ÍBranch-schema

F₁₂  |-  branch-name, assets → branch-name      

FD2 Augmentation: if F |- X → Y and W Í R, then F |- XW → YW.

F₁₂  |-  branch-name, assets → branch-name

And  branch-city Í Branch-schema

F₁₂  |-  branch-name, assets, branch-city → branch-name, branch-city

FD3 Transitivity: if F |- X → Y and F |- Y → Z, then F |- X → Z.

Let r₁ and r₂ be two relations over Banker-schema and Branch-schema. 
Consider the resulting relation of the join, r₁ |><| r₂ over the relation schema S=Banker-schema U Branch-schema.

r₁ |><| r₂ satisfies the following set F₁₂ of functional dependencies

branch-name → assets, branch-city
banker-id → branch-name
branch-name, customer-id → banker-id

We can have the following new proof to derive a new functional dependency:

(1) F₁₂ |- banker-id → branch-name
(2) F₁₂ |- branch-name → assets, branch-city |- branch-name → branch-city
(3) F₁₂ |- banker-id → branch-city by FD3

This implies that a banker who works in the Manhattan branch actually works in New York.

FD4 Union: if F |- X → Y and F |- X → Z, then F |- X → YZ.

Let r₁ and r₂ be two relations over Loan-schema and Borrower-schema. 
Consider the resulting relation of the join, r₁ |><| r₂ over the relation schema S = Loan-schema U Borrower-schema.

r₁ |><| r₂ satisfies the following set F₁₂ of functional dependencies

loan-number → amount, branch-name
loan-number → customer-id

We can have the following new proof to derive a new functional dependency:

(1)   F₁₂ |- loan-number → amount, branch-name

(2)   F₁₂ |- loan-number → customer-id

(3)   F₁₂ |- loan-number → customer-id, amount, branch-name by FD4

This implies that each loan of a certain amount of money is borrowed by a customer at a branch of the bank.

FD5 Decomposition: if F |- X → YZ, then F |- X → Y and F |- X → Z.

We can have the following new proof to derive two new functional dependencies for the relation schema, Customer-schema:

(1) F |- customer-id → customer-street, customer-city

(2) F |- customer-id → customer-street by FD5

(3) F |- customer-id → customer-city by FD5

 

FD6 Psuedo transitivity: if F |- X → Y and F |- YW → Z, then F |- XW → Z.

We can have the following new proof to derive two new functional dependencies for the relation schema, Banker-schema:

(1) F |- banker-id → branch-name

(2) F |- branch-name, customer-id → banker-id

(3) F |- branch-name, customer-id → branch-name by FD3 and (1)

(4) F |- banker-id, customer-id → branch-name by FD6 and (3)

This implies that a particular financial banker for a customer is appointed by a branch of the bank.