fa ⊃ ga ∙ (a ≠ a ∙ a ≠ a) ⌵ gb ∙ ([b|a][b|a] ∙ b ≠ b) ⌵ …
fb ⊃ ga ∙ ([a|b][a|b] ∙ a ≠ a) ⌵ gb ∙ (b ≠ b ∙ b ≠ b) ⌵ …
fc ⊃ – – – – – – – –
– – – – – – – ‒ ‒ ‒ &
& ga ⊃ fa(a ≠ a ∙ a ≠ a) ⌵ fb(b ≠ b ∙ a ≠ a) ⌵ …

fa ⊃ ga ∙ (a = a ∙ b = a) ⌵ gb ∙ (a = a ∙ b = b) ⌵ gc ∙ (a = a ∙ b = c) ⌵ ‒ ‒ ‒
fb ⊃ ga ∙ ([a|b] = a ∙ b = a) ⌵ gb ∙ (b = a ∙ b = b) ⌵ ‒ ‒ ‒
fc ⊃ ‒ ‒ ‒ ‒ ‒ ‒
– – – – –
g – – – – – –
fa ⊃ ga ∙ (a = a ∙ b = a . ⌵ . a = c ∙ d = a) ⌵ gb ∙ (a = a ∙ b = b . ⌵ . ‒ ‒ ‒


‒ ‒ ‒