:: FACIRC_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let IT be set ;
attr IT is pair means :Def1: :: FACIRC_1:def 1
ex x, y being set st IT = [x,y];
end;

:: deftheorem Def1 defines pair FACIRC_1:def 1 :
for IT being set holds
( IT is pair iff ex x, y being set st IT = [x,y] );

registration
cluster pair -> non empty set ;
coherence
for b1 being set st b1 is pair holds
not b1 is empty
proof end;
end;

registration
let x, y be set ;
cluster [x,y] -> pair ;
coherence
[x,y] is pair
proof end;
end;

registration
cluster non empty pair set ;
existence
ex b1 being set st b1 is pair
proof end;
cluster non pair set ;
existence
not for b1 being set holds b1 is pair
proof end;
end;

registration
cluster -> non pair Element of NAT ;
coherence
for b1 being Nat holds not b1 is pair
proof end;
end;

definition
let IT be set ;
attr IT is with_pair means :Def2: :: FACIRC_1:def 2
ex x being pair set st x in IT;
end;

:: deftheorem Def2 defines with_pair FACIRC_1:def 2 :
for IT being set holds
( IT is with_pair iff ex x being pair set st x in IT );

notation
let IT be set ;
antonym without_pairs IT for with_pair IT;
end;

registration
cluster empty -> without_pairs set ;
coherence
for b1 being set st b1 is empty holds
not b1 is with_pair
proof end;
let x be non pair set ;
cluster {x} -> without_pairs ;
coherence
not {x} is with_pair
proof end;
let y be non pair set ;
cluster {x,y} -> without_pairs ;
coherence
not {x,y} is with_pair
proof end;
let z be non pair set ;
cluster {x,y,z} -> without_pairs ;
coherence
not {x,y,z} is with_pair
proof end;
end;

registration
cluster non empty without_pairs set ;
existence
not for b1 being non empty set holds b1 is with_pair
proof end;
end;

registration
let X, Y be without_pairs set ;
cluster X \/ Y -> without_pairs ;
coherence
not X \/ Y is with_pair
proof end;
end;

registration
let X be without_pairs set ;
let Y be set ;
cluster X \ Y -> without_pairs ;
coherence
not X \ Y is with_pair
proof end;
cluster X /\ Y -> without_pairs ;
coherence
not X /\ Y is with_pair
proof end;
cluster Y /\ X -> without_pairs ;
coherence
not Y /\ X is with_pair
;
end;

registration
let x be pair set ;
cluster {x} -> Relation-like ;
coherence
{x} is Relation-like
proof end;
let y be pair set ;
cluster {x,y} -> Relation-like ;
coherence
{x,y} is Relation-like
proof end;
let z be pair set ;
cluster {x,y,z} -> Relation-like ;
coherence
{x,y,z} is Relation-like
proof end;
end;

registration
cluster Relation-like without_pairs -> empty without_pairs set ;
coherence
for b1 being set st not b1 is with_pair & b1 is Relation-like holds
b1 is empty
proof end;
end;

definition
let IT be Function;
attr IT is nonpair-yielding means :: FACIRC_1:def 3
for x being set st x in dom IT holds
not IT . x is pair;
end;

:: deftheorem defines nonpair-yielding FACIRC_1:def 3 :
for IT being Function holds
( IT is nonpair-yielding iff for x being set st x in dom IT holds
not IT . x is pair );

registration
let x be non pair set ;
cluster <*x*> -> nonpair-yielding ;
coherence
<*x*> is nonpair-yielding
proof end;
let y be non pair set ;
cluster <*x,y*> -> nonpair-yielding ;
coherence
<*x,y*> is nonpair-yielding
proof end;
let z be non pair set ;
cluster <*x,y,z*> -> nonpair-yielding ;
coherence
<*x,y,z*> is nonpair-yielding
proof end;
end;

theorem Th1: :: FACIRC_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function st f is nonpair-yielding holds
not rng f is with_pair
proof end;

registration
let n be Nat;
cluster one-to-one nonpair-yielding FinSeqLen of n;
existence
ex b1 being FinSeqLen of n st
( b1 is one-to-one & b1 is nonpair-yielding )
proof end;
end;

registration
cluster one-to-one nonpair-yielding set ;
existence
ex b1 being FinSequence st
( b1 is one-to-one & b1 is nonpair-yielding )
proof end;
end;

registration
let f be nonpair-yielding Function;
cluster rng f -> without_pairs ;
coherence
not rng f is with_pair
by Th1;
end;

theorem Th2: :: FACIRC_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InnerVertices S1 is Relation & InnerVertices S2 is Relation holds
InnerVertices (S1 +* S2) is Relation
proof end;

theorem Th3: :: FACIRC_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st InnerVertices S1 is Relation & InnerVertices S2 is Relation holds
InnerVertices (S1 +* S2) is Relation
proof end;

theorem Th4: :: FACIRC_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & InnerVertices S2 misses InputVertices S1 holds
( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
proof end;

theorem Th5: :: FACIRC_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, R being set st not X is with_pair & R is Relation holds
X misses R
proof end;

theorem Th6: :: FACIRC_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st not InputVertices S1 is with_pair & InnerVertices S2 is Relation holds
( InputVertices S1 c= InputVertices (S1 +* S2) & InputVertices (S1 +* S2) = (InputVertices S1) \/ ((InputVertices S2) \ (InnerVertices S1)) )
proof end;

theorem Th7: :: FACIRC_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st not InputVertices S1 is with_pair & InnerVertices S1 is Relation & not InputVertices S2 is with_pair & InnerVertices S2 is Relation holds
InputVertices (S1 +* S2) = (InputVertices S1) \/ (InputVertices S2)
proof end;

theorem Th8: :: FACIRC_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty ManySortedSign st S1 tolerates S2 & not InputVertices S1 is with_pair & not InputVertices S2 is with_pair holds
not InputVertices (S1 +* S2) is with_pair
proof end;

theorem Th9: :: FACIRC_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign st not InputVertices S1 is with_pair & not InputVertices S2 is with_pair holds
not InputVertices (S1 +* S2) is with_pair
proof end;

scheme :: FACIRC_1:sch 1
2AryBooleEx{ F1( set , set ) -> Element of BOOLEAN } :
ex f being Function of 2 -tuples_on BOOLEAN , BOOLEAN st
for x, y being Element of BOOLEAN holds f . <*x,y*> = F1(x,y)
proof end;

scheme :: FACIRC_1:sch 2
2AryBooleUniq{ F1( set , set ) -> Element of BOOLEAN } :
for f1, f2 being Function of 2 -tuples_on BOOLEAN , BOOLEAN st ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) holds
f1 = f2
proof end;

scheme :: FACIRC_1:sch 3
2AryBooleDef{ F1( set , set ) -> Element of BOOLEAN } :
( ex f being Function of 2 -tuples_on BOOLEAN , BOOLEAN st
for x, y being Element of BOOLEAN holds f . <*x,y*> = F1(x,y) & ( for f1, f2 being Function of 2 -tuples_on BOOLEAN , BOOLEAN st ( for x, y being Element of BOOLEAN holds f1 . <*x,y*> = F1(x,y) ) & ( for x, y being Element of BOOLEAN holds f2 . <*x,y*> = F1(x,y) ) holds
f1 = f2 ) )
proof end;

scheme :: FACIRC_1:sch 4
3AryBooleEx{ F1( set , set , set ) -> Element of BOOLEAN } :
ex f being Function of 3 -tuples_on BOOLEAN , BOOLEAN st
for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F1(x,y,z)
proof end;

scheme :: FACIRC_1:sch 5
3AryBooleUniq{ F1( set , set , set ) -> Element of BOOLEAN } :
for f1, f2 being Function of 3 -tuples_on BOOLEAN , BOOLEAN st ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) holds
f1 = f2
proof end;

scheme :: FACIRC_1:sch 6
3AryBooleDef{ F1( set , set , set ) -> Element of BOOLEAN } :
( ex f being Function of 3 -tuples_on BOOLEAN , BOOLEAN st
for x, y, z being Element of BOOLEAN holds f . <*x,y,z*> = F1(x,y,z) & ( for f1, f2 being Function of 3 -tuples_on BOOLEAN , BOOLEAN st ( for x, y, z being Element of BOOLEAN holds f1 . <*x,y,z*> = F1(x,y,z) ) & ( for x, y, z being Element of BOOLEAN holds f2 . <*x,y,z*> = F1(x,y,z) ) holds
f1 = f2 ) )
proof end;

definition
func 'xor' -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def4: :: FACIRC_1:def 4
for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'xor' y;
correctness
existence
ex b1 being Function of 2 -tuples_on BOOLEAN , BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y
;
uniqueness
for b1, b2 being Function of 2 -tuples_on BOOLEAN , BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'xor' y ) holds
b1 = b2
;
proof end;
func 'or' -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def5: :: FACIRC_1:def 5
for x, y being Element of BOOLEAN holds it . <*x,y*> = x 'or' y;
correctness
existence
ex b1 being Function of 2 -tuples_on BOOLEAN , BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y
;
uniqueness
for b1, b2 being Function of 2 -tuples_on BOOLEAN , BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x 'or' y ) holds
b1 = b2
;
proof end;
func '&' -> Function of 2 -tuples_on BOOLEAN , BOOLEAN means :Def6: :: FACIRC_1:def 6
for x, y being Element of BOOLEAN holds it . <*x,y*> = x '&' y;
correctness
existence
ex b1 being Function of 2 -tuples_on BOOLEAN , BOOLEAN st
for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y
;
uniqueness
for b1, b2 being Function of 2 -tuples_on BOOLEAN , BOOLEAN st ( for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y ) & ( for x, y being Element of BOOLEAN holds b2 . <*x,y*> = x '&' y ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def4 defines 'xor' FACIRC_1:def 4 :
for b1 being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds
( b1 = 'xor' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'xor' y );

:: deftheorem Def5 defines 'or' FACIRC_1:def 5 :
for b1 being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds
( b1 = 'or' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x 'or' y );

:: deftheorem Def6 defines '&' FACIRC_1:def 6 :
for b1 being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds
( b1 = '&' iff for x, y being Element of BOOLEAN holds b1 . <*x,y*> = x '&' y );

definition
func or3 -> Function of 3 -tuples_on BOOLEAN , BOOLEAN means :Def7: :: FACIRC_1:def 7
for x, y, z being Element of BOOLEAN holds it . <*x,y,z*> = (x 'or' y) 'or' z;
correctness
existence
ex b1 being Function of 3 -tuples_on BOOLEAN , BOOLEAN st
for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z
;
uniqueness
for b1, b2 being Function of 3 -tuples_on BOOLEAN , BOOLEAN st ( for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z ) & ( for x, y, z being Element of BOOLEAN holds b2 . <*x,y,z*> = (x 'or' y) 'or' z ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines or3 FACIRC_1:def 7 :
for b1 being Function of 3 -tuples_on BOOLEAN , BOOLEAN holds
( b1 = or3 iff for x, y, z being Element of BOOLEAN holds b1 . <*x,y,z*> = (x 'or' y) 'or' z );

definition
let x be set ;
:: original: <*
redefine func <*x*> -> FinSeqLen of 1;
coherence
<*x*> is FinSeqLen of 1
proof end;
let y be set ;
:: original: <*
redefine func <*x,y*> -> FinSeqLen of 2;
coherence
<*x,y*> is FinSeqLen of 2
proof end;
let z be set ;
:: original: <*
redefine func <*x,y,z*> -> FinSeqLen of 3;
coherence
<*x,y,z*> is FinSeqLen of 3
proof end;
end;

definition
let n, m be Nat;
let p be FinSeqLen of n;
let q be FinSeqLen of m;
:: original: ^
redefine func p ^ q -> FinSeqLen of n + m;
coherence
p ^ q is FinSeqLen of n + m
proof end;
end;

Lm1: now
let S be non empty non void ManySortedSign ; :: thesis: for o being Gate of S holds o in the OperSymbols of S
let o be Gate of S; :: thesis: o in the OperSymbols of S
not the OperSymbols of S is empty by MSUALG_1:def 5;
hence o in the OperSymbols of S ; :: thesis: verum
end;

theorem Th10: :: FACIRC_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (Den g,A) . (s * (the_arity_of g))
proof end;

definition
let S be non empty non void Circuit-like ManySortedSign ;
let A be non-empty Circuit of S;
let s be State of A;
let n be Nat;
func Following s,n -> State of A means :Def8: :: FACIRC_1:def 8
ex f being Function of NAT , product the Sorts of A st
( it = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) );
correctness
existence
ex b1 being State of A ex f being Function of NAT , product the Sorts of A st
( b1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) )
;
uniqueness
for b1, b2 being State of A st ex f being Function of NAT , product the Sorts of A st
( b1 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) & ex f being Function of NAT , product the Sorts of A st
( b2 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def8 defines Following FACIRC_1:def 8 :
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat
for b5 being State of A holds
( b5 = Following s,n iff ex f being Function of NAT , product the Sorts of A st
( b5 = f . n & f . 0 = s & ( for n being Nat holds f . (n + 1) = Following (f . n) ) ) );

theorem Th11: :: FACIRC_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following s,0 = s
proof end;

theorem Th12: :: FACIRC_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following s,(n + 1) = Following (Following s,n)
proof end;

theorem Th13: :: FACIRC_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n, m being Nat holds Following s,(n + m) = Following (Following s,n),m
proof end;

theorem Th14: :: FACIRC_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following s,1 = Following s
proof end;

theorem Th15: :: FACIRC_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds Following s,2 = Following (Following s)
proof end;

theorem Th16: :: FACIRC_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following s,(n + 1) = Following (Following s),n
proof end;

definition
let S be non empty non void Circuit-like ManySortedSign ;
let A be non-empty Circuit of S;
let s be State of A;
let x be set ;
pred s is_stable_at x means :Def9: :: FACIRC_1:def 9
for n being Nat holds (Following s,n) . x = s . x;
end;

:: deftheorem Def9 defines is_stable_at FACIRC_1:def 9 :
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set holds
( s is_stable_at x iff for n being Nat holds (Following s,n) . x = s . x );

theorem :: FACIRC_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set st s is_stable_at x holds
for n being Nat holds Following s,n is_stable_at x
proof end;

theorem :: FACIRC_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for x being set st x in InputVertices S holds
s is_stable_at x
proof end;

theorem Th19: :: FACIRC_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for g being Gate of S st ( for x being set st x in rng (the_arity_of g) holds
s is_stable_at x ) holds
Following s is_stable_at the_result_sort_of g
proof end;

theorem Th20: :: FACIRC_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty ManySortedSign
for v being Vertex of S1 holds
( v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1) )
proof end;

theorem Th21: :: FACIRC_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign
for x being set st x in InnerVertices S1 holds
( x in InnerVertices (S1 +* S2) & x in InnerVertices (S2 +* S1) )
proof end;

theorem :: FACIRC_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty ManySortedSign
for x being set st x in InnerVertices S2 holds
x in InnerVertices (S1 +* S2)
proof end;

theorem Th23: :: FACIRC_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds S1 +* S2 = S2 +* S1
proof end;

theorem Th24: :: FACIRC_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2 holds A1 +* A2 = A2 +* A1
proof end;

theorem Th25: :: FACIRC_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2, S3 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being Boolean Circuit of S1
for A2 being Boolean Circuit of S2
for A3 being Boolean Circuit of S3 holds (A1 +* A2) +* A3 = A1 +* (A2 +* A3)
proof end;

theorem Th26: :: FACIRC_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A1 being non-empty gate`2=den Boolean Circuit of S1
for A2 being non-empty gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2) holds
( s | the carrier of S1 is State of A1 & s | the carrier of S2 is State of A2 )
proof end;

theorem Th27: :: FACIRC_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty unsplit gate`1=arity ManySortedSign holds InnerVertices (S1 +* S2) = (InnerVertices S1) \/ (InnerVertices S2)
proof end;

theorem Th28: :: FACIRC_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
(Following s) | the carrier of S1 = Following s1
proof end;

theorem Th29: :: FACIRC_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
proof end;

theorem Th30: :: FACIRC_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following s,n) | the carrier of S1 = Following s1,n
proof end;

theorem Th31: :: FACIRC_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following s,n) | the carrier of S2 = Following s2,n
proof end;

theorem Th32: :: FACIRC_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S2 misses InputVertices S1 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for v being set st v in the carrier of S1 holds
for n being Nat holds (Following s,n) . v = (Following s1,n) . v
proof end;

theorem Th33: :: FACIRC_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st InnerVertices S1 misses InputVertices S2 holds
for A1 being gate`2=den Boolean Circuit of S1
for A2 being gate`2=den Boolean Circuit of S2
for s being State of (A1 +* A2)
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for v being set st v in the carrier of S2 holds
for n being Nat holds (Following s,n) . v = (Following s2,n) . v
proof end;

registration
let S be non empty non void gate`2=den ManySortedSign ;
let g be Gate of S;
cluster g `2 -> Relation-like Function-like ;
coherence
( g `2 is Function-like & g `2 is Relation-like )
proof end;
end;

theorem Th34: :: FACIRC_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void Circuit-like gate`2=den ManySortedSign
for A being non-empty Circuit of S st A is gate`2=den holds
for s being State of A
for g being Gate of S holds (Following s) . (the_result_sort_of g) = (g `2 ) . (s * (the_arity_of g))
proof end;

theorem Th35: :: FACIRC_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for f being Function st [p,f] in the OperSymbols of S holds
(Following s) . [p,f] = f . (s * p)
proof end;

theorem :: FACIRC_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being non-empty gate`2=den Boolean Circuit of S
for s being State of A
for p being FinSequence
for f being Function st [p,f] in the OperSymbols of S & ( for x being set st x in rng p holds
s is_stable_at x ) holds
Following s is_stable_at [p,f]
proof end;

theorem Th37: :: FACIRC_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty unsplit ManySortedSign holds InnerVertices S = the OperSymbols of S
proof end;

theorem Th38: :: FACIRC_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being set
for p being FinSequence holds InnerVertices (1GateCircStr p,f) is Relation
proof end;

theorem :: FACIRC_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being set
for p being nonpair-yielding FinSequence holds not InputVertices (1GateCircStr p,f) is with_pair
proof end;

theorem Th40: :: FACIRC_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, x, y being set holds InputVertices (1GateCircStr <*x,y*>,f) = {x,y}
proof end;

theorem Th41: :: FACIRC_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being set
for x, y being non pair set holds not InputVertices (1GateCircStr <*x,y*>,f) is with_pair
proof end;

theorem Th42: :: FACIRC_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, x, y, z being set holds InputVertices (1GateCircStr <*x,y,z*>,f) = {x,y,z}
proof end;

theorem Th43: :: FACIRC_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, f being set holds
( x in the carrier of (1GateCircStr <*x,y*>,f) & y in the carrier of (1GateCircStr <*x,y*>,f) & [<*x,y*>,f] in the carrier of (1GateCircStr <*x,y*>,f) )
proof end;

theorem Th44: :: FACIRC_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z, f being set holds
( x in the carrier of (1GateCircStr <*x,y,z*>,f) & y in the carrier of (1GateCircStr <*x,y,z*>,f) & z in the carrier of (1GateCircStr <*x,y,z*>,f) )
proof end;

theorem :: FACIRC_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, x being set
for p being FinSequence holds
( x in the carrier of (1GateCircStr p,f,x) & ( for y being set st y in rng p holds
y in the carrier of (1GateCircStr p,f,x) ) )
proof end;

theorem :: FACIRC_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, x being set
for p being FinSequence holds
( 1GateCircStr p,f,x is gate`1=arity & 1GateCircStr p,f,x is Circuit-like )
proof end;

theorem Th47: :: FACIRC_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for f being set holds [p,f] in InnerVertices (1GateCircStr p,f)
proof end;

definition
let x, y be set ;
let f be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
func 1GateCircuit x,y,f -> strict gate`2=den Boolean Circuit of 1GateCircStr <*x,y*>,f equals :: FACIRC_1:def 10
1GateCircuit <*x,y*>,f;
coherence
1GateCircuit <*x,y*>,f is strict gate`2=den Boolean Circuit of 1GateCircStr <*x,y*>,f
by CIRCCOMB:69;
end;

:: deftheorem defines 1GateCircuit FACIRC_1:def 10 :
for x, y being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds 1GateCircuit x,y,f = 1GateCircuit <*x,y*>,f;

theorem Th48: :: FACIRC_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for X being non empty finite set
for f being Function of 2 -tuples_on X,X
for s being State of (1GateCircuit <*x,y*>,f) holds
( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y )
proof end;

theorem Th49: :: FACIRC_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for X being non empty finite set
for f being Function of 2 -tuples_on X,X
for s being State of (1GateCircuit <*x,y*>,f) holds Following s is stable
proof end;

theorem Th50: :: FACIRC_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for s being State of (1GateCircuit x,y,f) holds
( (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y ) by Th48;

theorem :: FACIRC_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for s being State of (1GateCircuit x,y,f) holds Following s is stable by Th49;

definition
let x, y, z be set ;
let f be Function of 3 -tuples_on BOOLEAN , BOOLEAN ;
func 1GateCircuit x,y,z,f -> strict gate`2=den Boolean Circuit of 1GateCircStr <*x,y,z*>,f equals :: FACIRC_1:def 11
1GateCircuit <*x,y,z*>,f;
coherence
1GateCircuit <*x,y,z*>,f is strict gate`2=den Boolean Circuit of 1GateCircStr <*x,y,z*>,f
by CIRCCOMB:69;
end;

:: deftheorem defines 1GateCircuit FACIRC_1:def 11 :
for x, y, z being set
for f being Function of 3 -tuples_on BOOLEAN , BOOLEAN holds 1GateCircuit x,y,z,f = 1GateCircuit <*x,y,z*>,f;

theorem Th52: :: FACIRC_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set
for X being non empty finite set
for f being Function of 3 -tuples_on X,X
for s being State of (1GateCircuit <*x,y,z*>,f) holds
( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z )
proof end;

theorem Th53: :: FACIRC_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set
for X being non empty finite set
for f being Function of 3 -tuples_on X,X
for s being State of (1GateCircuit <*x,y,z*>,f) holds Following s is stable
proof end;

theorem :: FACIRC_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set
for f being Function of 3 -tuples_on BOOLEAN , BOOLEAN
for s being State of (1GateCircuit x,y,z,f) holds
( (Following s) . [<*x,y,z*>,f] = f . <*(s . x),(s . y),(s . z)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . z = s . z ) by Th52;

theorem :: FACIRC_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being set
for f being Function of 3 -tuples_on BOOLEAN , BOOLEAN
for s being State of (1GateCircuit x,y,z,f) holds Following s is stable by Th53;

definition
let x, y, c be set ;
let f be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
func 2GatesCircStr x,y,c,f -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 12
(1GateCircStr <*x,y*>,f) +* (1GateCircStr <*[<*x,y*>,f],c*>,f);
correctness
coherence
(1GateCircStr <*x,y*>,f) +* (1GateCircStr <*[<*x,y*>,f],c*>,f) is non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
;
end;

:: deftheorem defines 2GatesCircStr FACIRC_1:def 12 :
for x, y, c being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds 2GatesCircStr x,y,c,f = (1GateCircStr <*x,y*>,f) +* (1GateCircStr <*[<*x,y*>,f],c*>,f);

definition
let x, y, c be set ;
let f be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
func 2GatesCircOutput x,y,c,f -> Element of InnerVertices (2GatesCircStr x,y,c,f) equals :: FACIRC_1:def 13
[<*[<*x,y*>,f],c*>,f];
coherence
[<*[<*x,y*>,f],c*>,f] is Element of InnerVertices (2GatesCircStr x,y,c,f)
proof end;
correctness
;
end;

:: deftheorem defines 2GatesCircOutput FACIRC_1:def 13 :
for x, y, c being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds 2GatesCircOutput x,y,c,f = [<*[<*x,y*>,f],c*>,f];

registration
let x, y, c be set ;
let f be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
cluster 2GatesCircOutput x,y,c,f -> non empty pair ;
coherence
2GatesCircOutput x,y,c,f is pair
;
end;

theorem Th56: :: FACIRC_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds InnerVertices (2GatesCircStr x,y,c,f) = {[<*x,y*>,f],(2GatesCircOutput x,y,c,f)}
proof end;

theorem Th57: :: FACIRC_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c, x, y being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN st c <> [<*x,y*>,f] holds
InputVertices (2GatesCircStr x,y,c,f) = {x,y,c}
proof end;

definition
let x, y, c be set ;
let f be Function of 2 -tuples_on BOOLEAN , BOOLEAN ;
func 2GatesCircuit x,y,c,f -> strict gate`2=den Boolean Circuit of 2GatesCircStr x,y,c,f equals :: FACIRC_1:def 14
(1GateCircuit x,y,f) +* (1GateCircuit [<*x,y*>,f],c,f);
coherence
(1GateCircuit x,y,f) +* (1GateCircuit [<*x,y*>,f],c,f) is strict gate`2=den Boolean Circuit of 2GatesCircStr x,y,c,f
;
end;

:: deftheorem defines 2GatesCircuit FACIRC_1:def 14 :
for x, y, c being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds 2GatesCircuit x,y,c,f = (1GateCircuit x,y,f) +* (1GateCircuit [<*x,y*>,f],c,f);

theorem Th58: :: FACIRC_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds InnerVertices (2GatesCircStr x,y,c,f) is Relation
proof end;

theorem Th59: :: FACIRC_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for x, y, c being non pair set holds not InputVertices (2GatesCircStr x,y,c,f) is with_pair
proof end;

theorem Th60: :: FACIRC_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds
( x in the carrier of (2GatesCircStr x,y,c,f) & y in the carrier of (2GatesCircStr x,y,c,f) & c in the carrier of (2GatesCircStr x,y,c,f) )
proof end;

theorem :: FACIRC_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN holds
( [<*x,y*>,f] in the carrier of (2GatesCircStr x,y,c,f) & [<*[<*x,y*>,f],c*>,f] in the carrier of (2GatesCircStr x,y,c,f) )
proof end;

definition
let S be non empty non void unsplit ManySortedSign ;
let A be Boolean Circuit of S;
let s be State of A;
let v be Vertex of S;
:: original: .
redefine func s . v -> Element of BOOLEAN ;
coherence
s . v is Element of BOOLEAN
proof end;
end;

Lm2: for c, x, y being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for s being State of (2GatesCircuit x,y,c,f) st c <> [<*x,y*>,f] holds
( (Following s) . (2GatesCircOutput x,y,c,f) = f . <*(s . [<*x,y*>,f]),(s . c)*> & (Following s) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s) . x = s . x & (Following s) . y = s . y & (Following s) . c = s . c )
proof end;

theorem Th62: :: FACIRC_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c, x, y being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for s being State of (2GatesCircuit x,y,c,f) st c <> [<*x,y*>,f] holds
( (Following s,2) . (2GatesCircOutput x,y,c,f) = f . <*(f . <*(s . x),(s . y)*>),(s . c)*> & (Following s,2) . [<*x,y*>,f] = f . <*(s . x),(s . y)*> & (Following s,2) . x = s . x & (Following s,2) . y = s . y & (Following s,2) . c = s . c )
proof end;

theorem Th63: :: FACIRC_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c, x, y being set
for f being Function of 2 -tuples_on BOOLEAN , BOOLEAN
for s being State of (2GatesCircuit x,y,c,f) st c <> [<*x,y*>,f] holds
Following s,2 is stable
proof end;

theorem Th64: :: FACIRC_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c, x, y being set st c <> [<*x,y*>,'xor' ] holds
for s being State of (2GatesCircuit x,y,c,'xor' )
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following s,2) . (2GatesCircOutput x,y,c,'xor' ) = (a1 'xor' a2) 'xor' a3
proof end;

theorem :: FACIRC_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c, x, y being set st c <> [<*x,y*>,'or' ] holds
for s being State of (2GatesCircuit x,y,c,'or' )
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following s,2) . (2GatesCircOutput x,y,c,'or' ) = (a1 'or' a2) 'or' a3
proof end;

theorem :: FACIRC_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c, x, y being set st c <> [<*x,y*>,'&' ] holds
for s being State of (2GatesCircuit x,y,c,'&' )
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following s,2) . (2GatesCircOutput x,y,c,'&' ) = (a1 '&' a2) '&' a3
proof end;

definition
let x, y, c be set ;
func BitAdderOutput x,y,c -> Element of InnerVertices (2GatesCircStr x,y,c,'xor' ) equals :: FACIRC_1:def 15
2GatesCircOutput x,y,c,'xor' ;
coherence
2GatesCircOutput x,y,c,'xor' is Element of InnerVertices (2GatesCircStr x,y,c,'xor' )
;
end;

:: deftheorem defines BitAdderOutput FACIRC_1:def 15 :
for x, y, c being set holds BitAdderOutput x,y,c = 2GatesCircOutput x,y,c,'xor' ;

definition
let x, y, c be set ;
func BitAdderCirc x,y,c -> strict gate`2=den Boolean Circuit of 2GatesCircStr x,y,c,'xor' equals :: FACIRC_1:def 16
2GatesCircuit x,y,c,'xor' ;
coherence
2GatesCircuit x,y,c,'xor' is strict gate`2=den Boolean Circuit of 2GatesCircStr x,y,c,'xor'
;
end;

:: deftheorem defines BitAdderCirc FACIRC_1:def 16 :
for x, y, c being set holds BitAdderCirc x,y,c = 2GatesCircuit x,y,c,'xor' ;

definition
let x, y, c be set ;
func MajorityIStr x,y,c -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 17
((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) +* (1GateCircStr <*c,x*>,'&' );
correctness
coherence
((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) +* (1GateCircStr <*c,x*>,'&' ) is non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
;
end;

:: deftheorem defines MajorityIStr FACIRC_1:def 17 :
for x, y, c being set holds MajorityIStr x,y,c = ((1GateCircStr <*x,y*>,'&' ) +* (1GateCircStr <*y,c*>,'&' )) +* (1GateCircStr <*c,x*>,'&' );

definition
let x, y, c be set ;
func MajorityStr x,y,c -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 18
(MajorityIStr x,y,c) +* (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 );
correctness
coherence
(MajorityIStr x,y,c) +* (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ) is non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
;
end;

:: deftheorem defines MajorityStr FACIRC_1:def 18 :
for x, y, c being set holds MajorityStr x,y,c = (MajorityIStr x,y,c) +* (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 );

definition
let x, y, c be set ;
func MajorityICirc x,y,c -> strict gate`2=den Boolean Circuit of MajorityIStr x,y,c equals :: FACIRC_1:def 19
((1GateCircuit x,y,'&' ) +* (1GateCircuit y,c,'&' )) +* (1GateCircuit c,x,'&' );
coherence
((1GateCircuit x,y,'&' ) +* (1GateCircuit y,c,'&' )) +* (1GateCircuit c,x,'&' ) is strict gate`2=den Boolean Circuit of MajorityIStr x,y,c
;
end;

:: deftheorem defines MajorityICirc FACIRC_1:def 19 :
for x, y, c being set holds MajorityICirc x,y,c = ((1GateCircuit x,y,'&' ) +* (1GateCircuit y,c,'&' )) +* (1GateCircuit c,x,'&' );

theorem Th67: :: FACIRC_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds InnerVertices (MajorityStr x,y,c) is Relation
proof end;

theorem Th68: :: FACIRC_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds not InputVertices (MajorityStr x,y,c) is with_pair
proof end;

theorem :: FACIRC_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for s being State of (MajorityICirc x,y,c)
for a, b being Element of BOOLEAN st a = s . x & b = s . y holds
(Following s) . [<*x,y*>,'&' ] = a '&' b
proof end;

theorem :: FACIRC_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for s being State of (MajorityICirc x,y,c)
for a, b being Element of BOOLEAN st a = s . y & b = s . c holds
(Following s) . [<*y,c*>,'&' ] = a '&' b
proof end;

theorem :: FACIRC_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for s being State of (MajorityICirc x,y,c)
for a, b being Element of BOOLEAN st a = s . c & b = s . x holds
(Following s) . [<*c,x*>,'&' ] = a '&' b
proof end;

definition
let x, y, c be set ;
func MajorityOutput x,y,c -> Element of InnerVertices (MajorityStr x,y,c) equals :: FACIRC_1:def 20
[<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ];
coherence
[<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ] is Element of InnerVertices (MajorityStr x,y,c)
proof end;
correctness
;
end;

:: deftheorem defines MajorityOutput FACIRC_1:def 20 :
for x, y, c being set holds MajorityOutput x,y,c = [<*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ];

definition
let x, y, c be set ;
func MajorityCirc x,y,c -> strict gate`2=den Boolean Circuit of MajorityStr x,y,c equals :: FACIRC_1:def 21
(MajorityICirc x,y,c) +* (1GateCircuit [<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ],or3 );
coherence
(MajorityICirc x,y,c) +* (1GateCircuit [<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ],or3 ) is strict gate`2=den Boolean Circuit of MajorityStr x,y,c
;
end;

:: deftheorem defines MajorityCirc FACIRC_1:def 21 :
for x, y, c being set holds MajorityCirc x,y,c = (MajorityICirc x,y,c) +* (1GateCircuit [<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ],or3 );

theorem Th72: :: FACIRC_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds
( x in the carrier of (MajorityStr x,y,c) & y in the carrier of (MajorityStr x,y,c) & c in the carrier of (MajorityStr x,y,c) )
proof end;

theorem Th73: :: FACIRC_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds
( [<*x,y*>,'&' ] in InnerVertices (MajorityStr x,y,c) & [<*y,c*>,'&' ] in InnerVertices (MajorityStr x,y,c) & [<*c,x*>,'&' ] in InnerVertices (MajorityStr x,y,c) )
proof end;

theorem Th74: :: FACIRC_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds
( x in InputVertices (MajorityStr x,y,c) & y in InputVertices (MajorityStr x,y,c) & c in InputVertices (MajorityStr x,y,c) )
proof end;

theorem Th75: :: FACIRC_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds
( InputVertices (MajorityStr x,y,c) = {x,y,c} & InnerVertices (MajorityStr x,y,c) = {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} \/ {(MajorityOutput x,y,c)} )
proof end;

Lm3: for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s) . [<*x,y*>,'&' ] = a1 '&' a2 & (Following s) . [<*y,c*>,'&' ] = a2 '&' a3 & (Following s) . [<*c,x*>,'&' ] = a3 '&' a1 )
proof end;

theorem :: FACIRC_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s) . [<*x,y*>,'&' ] = a1 '&' a2
proof end;

theorem :: FACIRC_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following s) . [<*y,c*>,'&' ] = a2 '&' a3
proof end;

theorem :: FACIRC_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following s) . [<*c,x*>,'&' ] = a3 '&' a1
proof end;

theorem Th79: :: FACIRC_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . [<*x,y*>,'&' ] & a2 = s . [<*y,c*>,'&' ] & a3 = s . [<*c,x*>,'&' ] holds
(Following s) . (MajorityOutput x,y,c) = (a1 'or' a2) 'or' a3
proof end;

Lm4: for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) & (Following s,2) . [<*x,y*>,'&' ] = a1 '&' a2 & (Following s,2) . [<*y,c*>,'&' ] = a2 '&' a3 & (Following s,2) . [<*c,x*>,'&' ] = a3 '&' a1 )
proof end;

theorem :: FACIRC_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a1, a2 being Element of BOOLEAN st a1 = s . x & a2 = s . y holds
(Following s,2) . [<*x,y*>,'&' ] = a1 '&' a2
proof end;

theorem :: FACIRC_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a2, a3 being Element of BOOLEAN st a2 = s . y & a3 = s . c holds
(Following s,2) . [<*y,c*>,'&' ] = a2 '&' a3
proof end;

theorem :: FACIRC_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a1, a3 being Element of BOOLEAN st a1 = s . x & a3 = s . c holds
(Following s,2) . [<*c,x*>,'&' ] = a3 '&' a1
proof end;

theorem :: FACIRC_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
(Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) by Lm4;

theorem Th84: :: FACIRC_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (MajorityCirc x,y,c) holds Following s,2 is stable
proof end;

definition
let x, y, c be set ;
func BitAdderWithOverflowStr x,y,c -> non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign equals :: FACIRC_1:def 22
(2GatesCircStr x,y,c,'xor' ) +* (MajorityStr x,y,c);
coherence
(2GatesCircStr x,y,c,'xor' ) +* (MajorityStr x,y,c) is non empty strict non void unsplit gate`1=arity gate`2isBoolean ManySortedSign
;
end;

:: deftheorem defines BitAdderWithOverflowStr FACIRC_1:def 22 :
for x, y, c being set holds BitAdderWithOverflowStr x,y,c = (2GatesCircStr x,y,c,'xor' ) +* (MajorityStr x,y,c);

theorem Th85: :: FACIRC_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds InputVertices (BitAdderWithOverflowStr x,y,c) = {x,y,c}
proof end;

theorem :: FACIRC_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds InnerVertices (BitAdderWithOverflowStr x,y,c) = ({[<*x,y*>,'xor' ],(2GatesCircOutput x,y,c,'xor' )} \/ {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]}) \/ {(MajorityOutput x,y,c)}
proof end;

theorem :: FACIRC_1:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set
for S being non empty ManySortedSign st S = BitAdderWithOverflowStr x,y,c holds
( x in the carrier of S & y in the carrier of S & c in the carrier of S )
proof end;

definition
let x, y, c be set ;
func BitAdderWithOverflowCirc x,y,c -> strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr x,y,c equals :: FACIRC_1:def 23
(BitAdderCirc x,y,c) +* (MajorityCirc x,y,c);
coherence
(BitAdderCirc x,y,c) +* (MajorityCirc x,y,c) is strict gate`2=den Boolean Circuit of BitAdderWithOverflowStr x,y,c
;
end;

:: deftheorem defines BitAdderWithOverflowCirc FACIRC_1:def 23 :
for x, y, c being set holds BitAdderWithOverflowCirc x,y,c = (BitAdderCirc x,y,c) +* (MajorityCirc x,y,c);

theorem :: FACIRC_1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds InnerVertices (BitAdderWithOverflowStr x,y,c) is Relation
proof end;

theorem :: FACIRC_1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set holds not InputVertices (BitAdderWithOverflowStr x,y,c) is with_pair
proof end;

theorem :: FACIRC_1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being set holds
( BitAdderOutput x,y,c in InnerVertices (BitAdderWithOverflowStr x,y,c) & MajorityOutput x,y,c in InnerVertices (BitAdderWithOverflowStr x,y,c) ) by Th21;

theorem :: FACIRC_1:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BitAdderWithOverflowCirc x,y,c)
for a1, a2, a3 being Element of BOOLEAN st a1 = s . x & a2 = s . y & a3 = s . c holds
( (Following s,2) . (BitAdderOutput x,y,c) = (a1 'xor' a2) 'xor' a3 & (Following s,2) . (MajorityOutput x,y,c) = ((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1) )
proof end;

theorem :: FACIRC_1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, c being non pair set
for s being State of (BitAdderWithOverflowCirc x,y,c) holds Following s,2 is stable
proof end;