deffunc H1( object , object ) -> object = c1 `2 ;
let S be non empty ManySortedSign ; ( S is gate`2isBoolean implies S is gate`2=den )
assume A1:
for g being set st g in the carrier' of S holds
for p being FinSequence st p = the Arity of S . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
; CIRCCOMB:def 9 S is gate`2=den
A2:
now for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEANlet g be
set ;
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEANlet p be
Element of the
carrier of
S * ;
( g in the carrier' of S & p = the Arity of S . g implies H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN )assume that A3:
g in the
carrier' of
S
and A4:
p = the
Arity of
S . g
;
H1(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN
ex
f being
Function of
((len p) -tuples_on BOOLEAN),
BOOLEAN st
g = [(g `1),f]
by A1, A3, A4;
hence
H1(
g,
p) is
Function of
((len p) -tuples_on BOOLEAN),
BOOLEAN
;
verum end;
consider A being strict MSAlgebra over S such that
A5:
( the Sorts of A = the carrier of S --> BOOLEAN & ( for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
the Charact of A . g = H1(g,p) ) )
from CIRCCOMB:sch 2(A2);
take
A
; CIRCCOMB:def 11 A is gate`2=den
let g be set ; CIRCCOMB:def 10 ( g in the carrier' of S implies g = [(g `1),( the Charact of A . g)] )
assume A6:
g in the carrier' of S
; g = [(g `1),( the Charact of A . g)]
then reconsider p = the Arity of S . g as Element of the carrier of S * by FUNCT_2:5;
consider f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN such that
A7:
g = [(g `1),f]
by A1, A6;
f = g `2
by A7;
hence
g = [(g `1),( the Charact of A . g)]
by A5, A6, A7; verum