:: FTACELL1 semantic presentation begin definitionlet "ap", "bp", "cp", "dp", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA0Str"::: "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FTACELL1:def 1 (Set (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" "ap" "," "bp" "," "cp" ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" "ap" "," "bp" "," "cp" ")" ")" ) "," "cin" "," "dp" ")" ")" )); end; :: deftheorem defines :::"BitFTA0Str"::: FTACELL1:def 1 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ")" )))); definitionlet "ap", "bp", "cp", "dp", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA0Circ"::: "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" ) equals :: FTACELL1:def 2 (Set (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" "ap" "," "bp" "," "cp" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" "ap" "," "bp" "," "cp" ")" ")" ) "," "cin" "," "dp" ")" ")" )); end; :: deftheorem defines :::"BitFTA0Circ"::: FTACELL1:def 2 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_ftacell1 :::"BitFTA0Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k14_gfacirc1 :::"BitGFA0Circ"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ")" )))); theorem :: FTACELL1:1 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bp")) "," (Set (Var "cp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cp")) "," (Set (Var "ap")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k2_enumset1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ")" ) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: FTACELL1:2 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FTACELL1:3 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ($#k3_enumset1 :::"}"::: ) )))) ; theorem :: FTACELL1:4 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "ap")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "bp")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cp")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "dp")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bp")) "," (Set (Var "cp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cp")) "," (Set (Var "ap")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) ")" )) ; theorem :: FTACELL1:5 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bp")) "," (Set (Var "cp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cp")) "," (Set (Var "ap")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) ")" )) ; theorem :: FTACELL1:6 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ))))) "holds" (Bool "(" (Bool (Set (Var "ap")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "bp")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cp")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "dp")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) ")" ))) ; definitionlet "ap", "bp", "cp", "dp", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA0CarryOutput"::: "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" ")" )) equals :: FTACELL1:def 3 (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" "ap" "," "bp" "," "cp" ")" ); func :::"BitFTA0AdderOutputI"::: "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" ")" )) equals :: FTACELL1:def 4 (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" "ap" "," "bp" "," "cp" ")" ); func :::"BitFTA0AdderOutputP"::: "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" ")" )) equals :: FTACELL1:def 5 (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" "ap" "," "bp" "," "cp" ")" ")" ) "," "cin" "," "dp" ")" ); func :::"BitFTA0AdderOutputQ"::: "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k1_ftacell1 :::"BitFTA0Str"::: ) "(" "ap" "," "bp" "," "cp" "," "dp" "," "cin" ")" ")" )) equals :: FTACELL1:def 6 (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" "ap" "," "bp" "," "cp" ")" ")" ) "," "cin" "," "dp" ")" ); end; :: deftheorem defines :::"BitFTA0CarryOutput"::: FTACELL1:def 3 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_ftacell1 :::"BitFTA0CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ))); :: deftheorem defines :::"BitFTA0AdderOutputI"::: FTACELL1:def 4 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_ftacell1 :::"BitFTA0AdderOutputI"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ))); :: deftheorem defines :::"BitFTA0AdderOutputP"::: FTACELL1:def 5 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_ftacell1 :::"BitFTA0AdderOutputP"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_gfacirc1 :::"GFA0CarryOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ))); :: deftheorem defines :::"BitFTA0AdderOutputQ"::: FTACELL1:def 6 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k6_ftacell1 :::"BitFTA0AdderOutputQ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ))); theorem :: FTACELL1:7 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k2_ftacell1 :::"BitFTA0Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "ap")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bp")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cp"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_ftacell1 :::"BitFTA0CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a3")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a1")) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_ftacell1 :::"BitFTA0AdderOutputI"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")))) ")" ))))) ; theorem :: FTACELL1:8 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k2_ftacell1 :::"BitFTA0Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "ap")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bp")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cp")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "dp")))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "ap"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "bp"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "cp"))) ($#r1_hidden :::"="::: ) (Set (Var "a3"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "dp"))) ($#r1_hidden :::"="::: ) (Set (Var "a4"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))) ($#r1_hidden :::"="::: ) (Set (Var "a5"))) ")" ))))) ; theorem :: FTACELL1:9 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_gfacirc1 :::"BitGFA0Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k2_ftacell1 :::"BitFTA0Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "ap")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bp")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cp")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "dp")))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_ftacell1 :::"BitFTA0AdderOutputP"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a5")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a5")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a4")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a4")) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_ftacell1 :::"BitFTA0AdderOutputQ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a4")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a5")))) ")" ))))) ; theorem :: FTACELL1:10 (Bool "for" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k12_gfacirc1 :::"GFA0AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k2_ftacell1 :::"BitFTA0Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bp")) "," (Set (Var "cp")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; begin definitionlet "ap", "bm", "cp", "dm", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA1Str"::: "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FTACELL1:def 7 (Set (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" "ap" "," "bm" "," "cp" ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k37_gfacirc1 :::"BitGFA2Str"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" "ap" "," "bm" "," "cp" ")" ")" ) "," "cin" "," "dm" ")" ")" )); end; :: deftheorem defines :::"BitFTA1Str"::: FTACELL1:def 7 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k37_gfacirc1 :::"BitGFA2Str"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ")" )))); definitionlet "ap", "bm", "cp", "dm", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA1Circ"::: "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" ) equals :: FTACELL1:def 8 (Set (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" "ap" "," "bm" "," "cp" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k38_gfacirc1 :::"BitGFA2Circ"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" "ap" "," "bm" "," "cp" ")" ")" ) "," "cin" "," "dm" ")" ")" )); end; :: deftheorem defines :::"BitFTA1Circ"::: FTACELL1:def 8 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_ftacell1 :::"BitFTA1Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k38_gfacirc1 :::"BitGFA2Circ"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ")" )))); theorem :: FTACELL1:11 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bm")) "," (Set (Var "cp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cp")) "," (Set (Var "ap")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k2_enumset1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ")" ) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: FTACELL1:12 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FTACELL1:13 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ($#k3_enumset1 :::"}"::: ) )))) ; theorem :: FTACELL1:14 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "ap")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "bm")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cp")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "dm")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bm")) "," (Set (Var "cp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cp")) "," (Set (Var "ap")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) ")" )) ; theorem :: FTACELL1:15 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "ap")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bm")) "," (Set (Var "cp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cp")) "," (Set (Var "ap")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) ")" )) ; theorem :: FTACELL1:16 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ))))) "holds" (Bool "(" (Bool (Set (Var "ap")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "bm")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cp")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "dm")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) ")" ))) ; definitionlet "ap", "bm", "cp", "dm", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA1CarryOutput"::: "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" ")" )) equals :: FTACELL1:def 9 (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" "ap" "," "bm" "," "cp" ")" ); func :::"BitFTA1AdderOutputI"::: "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" ")" )) equals :: FTACELL1:def 10 (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" "ap" "," "bm" "," "cp" ")" ); func :::"BitFTA1AdderOutputP"::: "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" ")" )) equals :: FTACELL1:def 11 (Set ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" "ap" "," "bm" "," "cp" ")" ")" ) "," "cin" "," "dm" ")" ); func :::"BitFTA1AdderOutputQ"::: "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k7_ftacell1 :::"BitFTA1Str"::: ) "(" "ap" "," "bm" "," "cp" "," "dm" "," "cin" ")" ")" )) equals :: FTACELL1:def 12 (Set ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" "ap" "," "bm" "," "cp" ")" ")" ) "," "cin" "," "dm" ")" ); end; :: deftheorem defines :::"BitFTA1CarryOutput"::: FTACELL1:def 9 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_ftacell1 :::"BitFTA1CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ))); :: deftheorem defines :::"BitFTA1AdderOutputI"::: FTACELL1:def 10 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_ftacell1 :::"BitFTA1AdderOutputI"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ))); :: deftheorem defines :::"BitFTA1AdderOutputP"::: FTACELL1:def 11 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_ftacell1 :::"BitFTA1AdderOutputP"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ))); :: deftheorem defines :::"BitFTA1AdderOutputQ"::: FTACELL1:def 12 : (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_ftacell1 :::"BitFTA1AdderOutputQ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ))); theorem :: FTACELL1:17 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k8_ftacell1 :::"BitFTA1Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "ap")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bm")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cp"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k9_ftacell1 :::"BitFTA1CarryOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a3")) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a1")) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ftacell1 :::"BitFTA1AdderOutputI"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")) ")" ))) ")" ))))) ; theorem :: FTACELL1:18 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k8_ftacell1 :::"BitFTA1Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "ap")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bm")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cp")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "dm")))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "ap"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "bm"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "cp"))) ($#r1_hidden :::"="::: ) (Set (Var "a3"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "dm"))) ($#r1_hidden :::"="::: ) (Set (Var "a4"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))) ($#r1_hidden :::"="::: ) (Set (Var "a5"))) ")" ))))) ; theorem :: FTACELL1:19 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k8_ftacell1 :::"BitFTA1Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "ap")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bm")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cp")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "dm")))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k11_ftacell1 :::"BitFTA1AdderOutputP"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a5")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a5")) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a4")) ")" ) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a4")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k12_ftacell1 :::"BitFTA1AdderOutputQ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a3")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a4")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a5")))) ")" ))))) ; theorem :: FTACELL1:20 (Bool "for" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k8_ftacell1 :::"BitFTA1Circ"::: ) "(" (Set (Var "ap")) "," (Set (Var "bm")) "," (Set (Var "cp")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; begin definitionlet "am", "bp", "cm", "dp", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA2Str"::: "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FTACELL1:def 13 (Set (Set "(" ($#k37_gfacirc1 :::"BitGFA2Str"::: ) "(" "am" "," "bp" "," "cm" ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" "am" "," "bp" "," "cm" ")" ")" ) "," "cin" "," "dp" ")" ")" )); end; :: deftheorem defines :::"BitFTA2Str"::: FTACELL1:def 13 : (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k37_gfacirc1 :::"BitGFA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k25_gfacirc1 :::"BitGFA1Str"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ")" )))); definitionlet "am", "bp", "cm", "dp", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA2Circ"::: "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" ) equals :: FTACELL1:def 14 (Set (Set "(" ($#k38_gfacirc1 :::"BitGFA2Circ"::: ) "(" "am" "," "bp" "," "cm" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" "am" "," "bp" "," "cm" ")" ")" ) "," "cin" "," "dp" ")" ")" )); end; :: deftheorem defines :::"BitFTA2Circ"::: FTACELL1:def 14 : (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_ftacell1 :::"BitFTA2Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k38_gfacirc1 :::"BitGFA2Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k26_gfacirc1 :::"BitGFA1Circ"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ")" )))); theorem :: FTACELL1:21 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bp")) "," (Set (Var "cm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cm")) "," (Set (Var "am")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k2_enumset1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ")" ) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: FTACELL1:22 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FTACELL1:23 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k37_gfacirc1 :::"BitGFA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ($#k3_enumset1 :::"}"::: ) )))) ; theorem :: FTACELL1:24 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "am")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "bp")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cm")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "dp")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bp")) "," (Set (Var "cm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cm")) "," (Set (Var "am")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) ")" )) ; theorem :: FTACELL1:25 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bp")) "," (Set (Var "cm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cm")) "," (Set (Var "am")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_gfacirc1 :::"xor2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_gfacirc1 :::"and2c"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dp")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k3_twoscomp :::"and2a"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) ")" )) ; theorem :: FTACELL1:26 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k37_gfacirc1 :::"BitGFA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ))))) "holds" (Bool "(" (Bool (Set (Var "am")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "bp")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cm")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "dp")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ))) ")" ))) ; definitionlet "am", "bp", "cm", "dp", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA2CarryOutput"::: "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" ")" )) equals :: FTACELL1:def 15 (Set ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" "am" "," "bp" "," "cm" ")" ); func :::"BitFTA2AdderOutputI"::: "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" ")" )) equals :: FTACELL1:def 16 (Set ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" "am" "," "bp" "," "cm" ")" ); func :::"BitFTA2AdderOutputP"::: "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" ")" )) equals :: FTACELL1:def 17 (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" "am" "," "bp" "," "cm" ")" ")" ) "," "cin" "," "dp" ")" ); func :::"BitFTA2AdderOutputQ"::: "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k13_ftacell1 :::"BitFTA2Str"::: ) "(" "am" "," "bp" "," "cm" "," "dp" "," "cin" ")" ")" )) equals :: FTACELL1:def 18 (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" "am" "," "bp" "," "cm" ")" ")" ) "," "cin" "," "dp" ")" ); end; :: deftheorem defines :::"BitFTA2CarryOutput"::: FTACELL1:def 15 : (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k15_ftacell1 :::"BitFTA2CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k33_gfacirc1 :::"GFA2CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ))); :: deftheorem defines :::"BitFTA2AdderOutputI"::: FTACELL1:def 16 : (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k16_ftacell1 :::"BitFTA2AdderOutputI"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ))); :: deftheorem defines :::"BitFTA2AdderOutputP"::: FTACELL1:def 17 : (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k17_ftacell1 :::"BitFTA2AdderOutputP"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k21_gfacirc1 :::"GFA1CarryOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ))); :: deftheorem defines :::"BitFTA2AdderOutputQ"::: FTACELL1:def 18 : (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k18_ftacell1 :::"BitFTA2AdderOutputQ"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k24_gfacirc1 :::"GFA1AdderOutput"::: ) "(" (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dp")) ")" ))); theorem :: FTACELL1:27 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "dp")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k14_ftacell1 :::"BitFTA2Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "am")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bp")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cm"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k15_ftacell1 :::"BitFTA2CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a2")) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a2")) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k16_ftacell1 :::"BitFTA2AdderOutputI"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ))) ")" ))))) ; theorem :: FTACELL1:28 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k37_gfacirc1 :::"BitGFA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k14_ftacell1 :::"BitFTA2Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "am")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bp")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cm")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "dp")))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "am"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "bp"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "cm"))) ($#r1_hidden :::"="::: ) (Set (Var "a3"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "dp"))) ($#r1_hidden :::"="::: ) (Set (Var "a4"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))) ($#r1_hidden :::"="::: ) (Set (Var "a5"))) ")" ))))) ; theorem :: FTACELL1:29 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k37_gfacirc1 :::"BitGFA2Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k14_ftacell1 :::"BitFTA2Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "am")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bp")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cm")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "dp")))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k17_ftacell1 :::"BitFTA2AdderOutputP"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a5")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a5")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set (Var "a4")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set (Var "a4")) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k18_ftacell1 :::"BitFTA2AdderOutputQ"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a2")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set (Var "a4")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a5")) ")" ) ")" ))) ")" ))))) ; theorem :: FTACELL1:30 (Bool "for" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dp")) "," (Set "(" ($#k36_gfacirc1 :::"GFA2AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k2_twoscomp :::"and2"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k14_ftacell1 :::"BitFTA2Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bp")) "," (Set (Var "cm")) "," (Set (Var "dp")) "," (Set (Var "cin")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))) ; begin definitionlet "am", "bm", "cm", "dm", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA3Str"::: "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ($#v2_circcomb :::"gate`1=arity"::: ) ($#v3_circcomb :::"gate`2isBoolean"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: FTACELL1:def 19 (Set (Set "(" ($#k49_gfacirc1 :::"BitGFA3Str"::: ) "(" "am" "," "bm" "," "cm" ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k49_gfacirc1 :::"BitGFA3Str"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" "am" "," "bm" "," "cm" ")" ")" ) "," "cin" "," "dm" ")" ")" )); end; :: deftheorem defines :::"BitFTA3Str"::: FTACELL1:def 19 : (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k49_gfacirc1 :::"BitGFA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" ($#k49_gfacirc1 :::"BitGFA3Str"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ")" )))); definitionlet "am", "bm", "cm", "dm", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA3Circ"::: "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_circcomb :::"gate`2=den"::: ) ($#v6_circcomb :::"Boolean"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" ) equals :: FTACELL1:def 20 (Set (Set "(" ($#k50_gfacirc1 :::"BitGFA3Circ"::: ) "(" "am" "," "bm" "," "cm" ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k50_gfacirc1 :::"BitGFA3Circ"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" "am" "," "bm" "," "cm" ")" ")" ) "," "cin" "," "dm" ")" ")" )); end; :: deftheorem defines :::"BitFTA3Circ"::: FTACELL1:def 20 : (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k20_ftacell1 :::"BitFTA3Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k50_gfacirc1 :::"BitGFA3Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" ($#k50_gfacirc1 :::"BitGFA3Circ"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ")" )))); theorem :: FTACELL1:31 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bm")) "," (Set (Var "cm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cm")) "," (Set (Var "am")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k2_enumset1 :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ")" ) ($#k2_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ")" ) ($#k2_enumset1 :::"}"::: ) )))) ; theorem :: FTACELL1:32 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) "is" ($#m1_hidden :::"Relation":::))) ; theorem :: FTACELL1:33 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k49_gfacirc1 :::"BitGFA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ))))) "holds" (Bool (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_enumset1 :::"{"::: ) (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ($#k3_enumset1 :::"}"::: ) )))) ; theorem :: FTACELL1:34 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "am")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "bm")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cm")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "dm")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bm")) "," (Set (Var "cm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cm")) "," (Set (Var "am")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) ")" )) ; theorem :: FTACELL1:35 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "am")) "," (Set (Var "bm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "bm")) "," (Set (Var "cm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cm")) "," (Set (Var "am")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k14_twoscomp :::"xor2"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "cin")) "," (Set (Var "dm")) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) ")" )) ; theorem :: FTACELL1:36 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k49_gfacirc1 :::"BitGFA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ))))) "holds" (Bool "(" (Bool (Set (Var "am")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "bm")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cm")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "dm")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) & (Bool (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ))) ")" ))) ; definitionlet "am", "bm", "cm", "dm", "cin" be ($#m1_hidden :::"set"::: ) ; func :::"BitFTA3CarryOutput"::: "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" ")" )) equals :: FTACELL1:def 21 (Set ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" "am" "," "bm" "," "cm" ")" ); func :::"BitFTA3AdderOutputI"::: "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" ")" )) equals :: FTACELL1:def 22 (Set ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" "am" "," "bm" "," "cm" ")" ); func :::"BitFTA3AdderOutputP"::: "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" ")" )) equals :: FTACELL1:def 23 (Set ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" "am" "," "bm" "," "cm" ")" ")" ) "," "cin" "," "dm" ")" ); func :::"BitFTA3AdderOutputQ"::: "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k19_ftacell1 :::"BitFTA3Str"::: ) "(" "am" "," "bm" "," "cm" "," "dm" "," "cin" ")" ")" )) equals :: FTACELL1:def 24 (Set ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" "am" "," "bm" "," "cm" ")" ")" ) "," "cin" "," "dm" ")" ); end; :: deftheorem defines :::"BitFTA3CarryOutput"::: FTACELL1:def 21 : (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k21_ftacell1 :::"BitFTA3CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ))); :: deftheorem defines :::"BitFTA3AdderOutputI"::: FTACELL1:def 22 : (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k22_ftacell1 :::"BitFTA3AdderOutputI"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ))); :: deftheorem defines :::"BitFTA3AdderOutputP"::: FTACELL1:def 23 : (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k23_ftacell1 :::"BitFTA3AdderOutputP"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k45_gfacirc1 :::"GFA3CarryOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ))); :: deftheorem defines :::"BitFTA3AdderOutputQ"::: FTACELL1:def 24 : (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k24_ftacell1 :::"BitFTA3AdderOutputQ"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) "," (Set (Var "cin")) "," (Set (Var "dm")) ")" ))); theorem :: FTACELL1:37 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "dm")) "," (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k20_ftacell1 :::"BitFTA3Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "am")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bm")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cm"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k21_ftacell1 :::"BitFTA3CarryOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k22_ftacell1 :::"BitFTA3AdderOutputI"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ))) ")" ))))) ; theorem :: FTACELL1:38 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k49_gfacirc1 :::"BitGFA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k20_ftacell1 :::"BitFTA3Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "am")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bm")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cm")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "dm")))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "am"))) ($#r1_hidden :::"="::: ) (Set (Var "a1"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "bm"))) ($#r1_hidden :::"="::: ) (Set (Var "a2"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "cm"))) ($#r1_hidden :::"="::: ) (Set (Var "a3"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "dm"))) ($#r1_hidden :::"="::: ) (Set (Var "a4"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 2) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))) ($#r1_hidden :::"="::: ) (Set (Var "a5"))) ")" ))))) ; theorem :: FTACELL1:39 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Bool "not" (Set (Var "cin")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set "(" ($#k49_gfacirc1 :::"BitGFA3Str"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k20_ftacell1 :::"BitFTA3Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "am")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "bm")))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cm")))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "dm")))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "cin"))))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k23_ftacell1 :::"BitFTA3AdderOutputP"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a5")) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a5")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a4")) ")" ) ")" ) ")" ) ($#k1_binarith :::"'or'"::: ) (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a4")) ")" ) ($#k10_margrel1 :::"'&'"::: ) (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k24_ftacell1 :::"BitFTA3AdderOutputQ"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_margrel1 :::"'not'"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a1")) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a2")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a3")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a4")) ")" ) ")" ) ($#k2_binarith :::"'xor'"::: ) (Set "(" ($#k9_margrel1 :::"'not'"::: ) (Set (Var "a5")) ")" ) ")" ))) ")" ))))) ; theorem :: FTACELL1:40 (Bool "for" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "being" ($#~v1_xtuple_0 "non" ($#v1_xtuple_0 :::"pair"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "cin")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "cin")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "dm")) "," (Set "(" ($#k48_gfacirc1 :::"GFA3AdderOutput"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) "," (Set ($#k4_twoscomp :::"and2b"::: ) ) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" ($#k20_ftacell1 :::"BitFTA3Circ"::: ) "(" (Set (Var "am")) "," (Set (Var "bm")) "," (Set (Var "cm")) "," (Set (Var "dm")) "," (Set (Var "cin")) ")" ")" ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Num 4) ")" ) "is" ($#v1_circuit2 :::"stable"::: ) )))) ;