defpred S1[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is DecoratedTree of & $4 is DecoratedTree of implies ex p', q' being DecoratedTree of st
( p' = $3 & q' = $4 & $5 = ($1 '&' $2) -tree p',q' ) ) & ( ( not $3 is DecoratedTree of or not $4 is DecoratedTree of ) implies $5 = {} ) );
defpred S2[ Element of HP-WFF , Element of HP-WFF , set , set , set ] means ( ( $3 is DecoratedTree of & $4 is DecoratedTree of implies ex p', q' being DecoratedTree of st
( p' = $3 & q' = $4 & $5 = ($1 => $2) -tree p',q' ) ) & ( ( not $3 is DecoratedTree of or not $4 is DecoratedTree of ) implies $5 = {} ) );
A1: for p, q being Element of HP-WFF
for a, b being set ex c being set st S1[p,q,a,b,c]
proof
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex c being set st S1[p,q,a,b,c]
let a, b be set ; :: thesis: ex c being set st S1[p,q,a,b,c]
per cases ( ( a is DecoratedTree of & b is DecoratedTree of ) or not a is DecoratedTree of or not b is DecoratedTree of ) ;
suppose that A2: a is DecoratedTree of and
A3: b is DecoratedTree of ; :: thesis: ex c being set st S1[p,q,a,b,c]
reconsider p' = a as DecoratedTree of by A2;
reconsider q' = b as DecoratedTree of by A3;
take (p '&' q) -tree p',q' ; :: thesis: S1[p,q,a,b,(p '&' q) -tree p',q']
thus S1[p,q,a,b,(p '&' q) -tree p',q'] ; :: thesis: verum
end;
suppose ( not a is DecoratedTree of or not b is DecoratedTree of ) ; :: thesis: ex c being set st S1[p,q,a,b,c]
hence ex c being set st S1[p,q,a,b,c] ; :: thesis: verum
end;
end;
end;
A4: for p, q being Element of HP-WFF
for a, b being set ex d being set st S2[p,q,a,b,d]
proof
let p, q be Element of HP-WFF ; :: thesis: for a, b being set ex d being set st S2[p,q,a,b,d]
let a, b be set ; :: thesis: ex d being set st S2[p,q,a,b,d]
per cases ( ( a is DecoratedTree of & b is DecoratedTree of ) or not a is DecoratedTree of or not b is DecoratedTree of ) ;
suppose that A5: a is DecoratedTree of and
A6: b is DecoratedTree of ; :: thesis: ex d being set st S2[p,q,a,b,d]
reconsider p' = a as DecoratedTree of by A5;
reconsider q' = b as DecoratedTree of by A6;
take (p => q) -tree p',q' ; :: thesis: S2[p,q,a,b,(p => q) -tree p',q']
thus S2[p,q,a,b,(p => q) -tree p',q'] ; :: thesis: verum
end;
suppose ( not a is DecoratedTree of or not b is DecoratedTree of ) ; :: thesis: ex d being set st S2[p,q,a,b,d]
hence ex d being set st S2[p,q,a,b,d] ; :: thesis: verum
end;
end;
end;
A7: for p, q being Element of HP-WFF
for a, b, c, d being set st S1[p,q,a,b,c] & S1[p,q,a,b,d] holds
c = d ;
A8: for p, q being Element of HP-WFF
for a, b, c, d being set st S2[p,q,a,b,c] & S2[p,q,a,b,d] holds
c = d ;
deffunc H1( Element of NAT ) -> Element of FinTrees HP-WFF = root-tree (prop $1);
consider M being ManySortedSet of such that
A9: M . VERUM = root-tree VERUM and
A10: for n being Element of NAT holds M . (prop n) = H1(n) and
A11: for p, q being Element of HP-WFF holds
( S1[p,q,M . p,M . q,M . (p '&' q)] & S2[p,q,M . p,M . q,M . (p => q)] ) from HILBERT2:sch 3(A1, A4, A7, A8);
 take M ; :: thesis: ( M . VERUM = root-tree VERUM & ( for n being Element of NAT holds M . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of st
( p' = M . p & q' = M . q & M . (p '&' q) = (p '&' q) -tree p',q' & M . (p => q) = (p => q) -tree p',q' ) ) )
thus M . VERUM = root-tree VERUM by A9; :: thesis: ( ( for n being Element of NAT holds M . (prop n) = root-tree (prop n) ) & ( for p, q being Element of HP-WFF ex p', q' being DecoratedTree of st
( p' = M . p & q' = M . q & M . (p '&' q) = (p '&' q) -tree p',q' & M . (p => q) = (p => q) -tree p',q' ) ) )
thus for n being Element of NAT holds M . (prop n) = root-tree (prop n) by A10; :: thesis: for p, q being Element of HP-WFF ex p', q' being DecoratedTree of st
( p' = M . p & q' = M . q & M . (p '&' q) = (p '&' q) -tree p',q' & M . (p => q) = (p => q) -tree p',q' )
let p, q be Element of HP-WFF ; :: thesis: ex p', q' being DecoratedTree of st
( p' = M . p & q' = M . q & M . (p '&' q) = (p '&' q) -tree p',q' & M . (p => q) = (p => q) -tree p',q' )
defpred S3[ Element of HP-WFF ] means M . $1 is DecoratedTree of ;
A12: S3[ VERUM ] by A9;
A13: for n being Element of NAT holds S3[ prop n]
proof
let n be Element of NAT ; :: thesis: S3[ prop n]
M . (prop n) = root-tree (prop n) by A10;
hence S3[ prop n] ; :: thesis: verum
end;
A14: for r, s being Element of HP-WFF st S3[r] & S3[s] holds
( S3[r '&' s] & S3[r => s] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S3[r] & S3[s] implies ( S3[r '&' s] & S3[r => s] ) )
assume that
A15: M . r is DecoratedTree of and
A16: M . s is DecoratedTree of ; :: thesis: ( S3[r '&' s] & S3[r => s] )
S1[r,s,M . r,M . s,M . (r '&' s)] by A11;
hence M . (r '&' s) is DecoratedTree of by A15, A16; :: thesis: S3[r => s]
S2[r,s,M . r,M . s,M . (r => s)] by A11;
hence S3[r => s] by A15, A16; :: thesis: verum
end;
A17: for p being Element of HP-WFF holds S3[p] from HILBERT2:sch 2(A12, A13, A14);
 ( S1[p,q,M . p,M . q,M . (p '&' q)] & S2[p,q,M . p,M . q,M . (p => q)] ) by A11;
hence ex p', q' being DecoratedTree of st
( p' = M . p & q' = M . q & M . (p '&' q) = (p '&' q) -tree p',q' & M . (p => q) = (p => q) -tree p',q' ) by A17; :: thesis: verum