:: STACKS_1 semantic presentation begin definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "s1", "s2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "A")); :: original: :::"^"::: redefine func "s1" :::"^"::: "s2" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "A" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "i" be ($#m1_hidden :::"Nat":::); let "s" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "A")); :: original: :::"Del"::: redefine func :::"Del"::: "(" "s" "," "i" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "A" ($#k3_finseq_2 :::"*"::: ) ); end; theorem :: STACKS_1:1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; scheme :: STACKS_1:sch 1 IndSeqD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "p"))])) provided (Bool P1[(Set ($#k6_finseq_1 :::"<*>"::: ) (Set F1 "(" ")" ))]) and (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "p"))])) "holds" (Bool P1[(Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_stacks_1 :::"^"::: ) (Set (Var "p")))]))) proof end; definitionlet "C", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_hidden :::"Relation":::); mode :::"BinOp"::: "of" "C" "," "D" "," "R" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "C" "," "D" ($#k2_zfmisc_1 :::":]"::: ) ) "," "D" means :: STACKS_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y2")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R"))); end; :: deftheorem defines :::"BinOp"::: STACKS_1:def 1 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_stacks_1 :::"BinOp"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "R"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "b4")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y1")) ")" ")" ) "," (Set "(" (Set (Var "b4")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y2")) ")" ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))))) ")" )))); scheme :: STACKS_1:sch 2 LambdaD2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "holds" (Bool (Set (Set (Var "M")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "i")) "," (Set (Var "j")) ")" ))))) proof end; definitionlet "C", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "D")); let "b" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "D")); assume (Bool (Set (Const "b")) "is" ($#m1_stacks_1 :::"BinOp"::: ) "of" (Set (Const "C")) "," (Set (Const "D")) "," (Set (Const "R"))) ; func "b" :::"/\/"::: "R" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "C" "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "R" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "R" ")" ) means :: STACKS_1:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "C") & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) "R")) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set (Var "y")))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" "R" "," (Set "(" "b" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y1")) ")" ")" ) ")" ))); end; :: deftheorem defines :::"/\/"::: STACKS_1:def 2 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "b")) "is" ($#m1_stacks_1 :::"BinOp"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "R")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_stacks_1 :::"/\/"::: ) (Set (Var "R")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "C"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "R")))) & (Bool (Set (Var "y1")) ($#r2_hidden :::"in"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "b")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y1")) ")" ")" ) ")" ))) ")" ))))); definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "C" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); let "D" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "B")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"+*"::: redefine func "f" :::"+*"::: "g" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "B"; end; begin definitionattr "c1" is :::"strict"::: ; struct :::"StackSystem"::: -> ($#l5_struct_0 :::"2-sorted"::: ) ; aggr :::"StackSystem":::(# :::"carrier":::, :::"carrier'":::, :::"s_empty":::, :::"s_push":::, :::"s_pop":::, :::"s_top"::: #) -> ($#l1_stacks_1 :::"StackSystem"::: ) ; sel :::"s_empty"::: "c1" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); sel :::"s_push"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); sel :::"s_pop"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); sel :::"s_top"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registrationlet "a1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a2" be ($#m1_hidden :::"set"::: ) ; let "a3" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "a2")); let "a4" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "a1")) "," (Set (Const "a2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "a2")); let "a5" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "a2")) "," (Set (Const "a2")); let "a6" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "a2")) "," (Set (Const "a1")); cluster (Set ($#g1_stacks_1 :::"StackSystem"::: ) "(#" "a1" "," "a2" "," "a3" "," "a4" "," "a5" "," "a6" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "a1" be ($#m1_hidden :::"set"::: ) ; let "a2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a3" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "a2")); let "a4" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "a1")) "," (Set (Const "a2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "a2")); let "a5" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "a2")) "," (Set (Const "a2")); let "a6" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "a2")) "," (Set (Const "a1")); cluster (Set ($#g1_stacks_1 :::"StackSystem"::: ) "(#" "a1" "," "a2" "," "a3" "," "a4" "," "a5" "," "a6" "#)" ) -> ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) for ($#l1_stacks_1 :::"StackSystem"::: ) ; end; definitionlet "X" be ($#l1_stacks_1 :::"StackSystem"::: ) ; mode stack of "X" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X"); end; definitionlet "X" be ($#l1_stacks_1 :::"StackSystem"::: ) ; let "s" be ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")); pred :::"emp"::: "s" means :: STACKS_1:def 3 (Bool "s" ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" "X")); end; :: deftheorem defines :::"emp"::: STACKS_1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackSystem"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" (Set (Var "X")))) ")" ))); definitionlet "X" be ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) ; let "s" be ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")); func :::"pop"::: "s" -> ($#m1_subset_1 :::"stack":::) "of" "X" equals :: STACKS_1:def 4 (Set (Set "the" ($#u3_stacks_1 :::"s_pop"::: ) "of" "X") ($#k3_funct_2 :::"."::: ) "s"); func :::"top"::: "s" -> ($#m1_subset_1 :::"Element":::) "of" "X" equals :: STACKS_1:def 5 (Set (Set "the" ($#u4_stacks_1 :::"s_top"::: ) "of" "X") ($#k3_funct_2 :::"."::: ) "s"); end; :: deftheorem defines :::"pop"::: STACKS_1:def 4 : (Bool "for" (Set (Var "X")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_stacks_1 :::"s_pop"::: ) "of" (Set (Var "X"))) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))))); :: deftheorem defines :::"top"::: STACKS_1:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_stacks_1 :::"s_top"::: ) "of" (Set (Var "X"))) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))))); definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) ; let "s" be ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")); let "e" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"push"::: "(" "e" "," "s" ")" -> ($#m1_subset_1 :::"stack":::) "of" "X" equals :: STACKS_1:def 6 (Set (Set "the" ($#u2_stacks_1 :::"s_push"::: ) "of" "X") ($#k2_binop_1 :::"."::: ) "(" "e" "," "s" ")" ); end; :: deftheorem defines :::"push"::: STACKS_1:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_stacks_1 :::"s_push"::: ) "of" (Set (Var "X"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ))))); definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"StandardStackSystem"::: "A" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ($#l1_stacks_1 :::"StackSystem"::: ) means :: STACKS_1:def 7 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) "A") & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "A" ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" it "holds" (Bool "(" "(" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) "implies" (Bool (Set (Var "s")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "s")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))) ")" & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "implies" (Bool "(" (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "g")) "," (Num 1) ")" )) ")" ) ")" & "(" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) "implies" (Bool "(" (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Element":::) "of" it) & (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" it "holds" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "g")))) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"StandardStackSystem"::: STACKS_1:def 7 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ($#l1_stacks_1 :::"StackSystem"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "b2")) "holds" (Bool "(" "(" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) "implies" (Bool (Set (Var "s")) "is" ($#v1_xboole_0 :::"empty"::: ) ) ")" & "(" (Bool (Bool (Set (Var "s")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "implies" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))) ")" & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "implies" (Bool "(" (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "g")) "," (Num 1) ")" )) ")" ) ")" & "(" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) "implies" (Bool "(" (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2"))) & (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "b2")) "holds" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "g")))) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k8_stacks_1 :::"StandardStackSystem"::: ) "A" ")" )) -> ($#v4_funct_1 :::"functional"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k8_stacks_1 :::"StandardStackSystem"::: ) "A" ")" )); end; definitionlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) ; attr "X" is :::"pop-finite"::: means :: STACKS_1:def 8 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X") (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::)(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "implies" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")))) ")" ")" )))); attr "X" is :::"push-pop"::: means :: STACKS_1:def 9 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" "st" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set "(" ($#k6_stacks_1 :::"top"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")) ")" ) ")" ))); attr "X" is :::"top-push"::: means :: STACKS_1:def 10 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k6_stacks_1 :::"top"::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ")" ))))); attr "X" is :::"pop-push"::: means :: STACKS_1:def 11 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ")" ))))); attr "X" is :::"push-non-empty"::: means :: STACKS_1:def 12 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ))))); end; :: deftheorem defines :::"pop-finite"::: STACKS_1:def 8 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_stacks_1 :::"pop-finite"::: ) ) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X"))) (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::)(Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "implies" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")))) ")" ")" )))) ")" )); :: deftheorem defines :::"push-pop"::: STACKS_1:def 9 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_stacks_1 :::"push-pop"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set "(" ($#k6_stacks_1 :::"top"::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")) ")" ) ")" ))) ")" )); :: deftheorem defines :::"top-push"::: STACKS_1:def 10 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_stacks_1 :::"top-push"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k6_stacks_1 :::"top"::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ")" ))))) ")" )); :: deftheorem defines :::"pop-push"::: STACKS_1:def 11 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_stacks_1 :::"pop-push"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ")" ))))) ")" )); :: deftheorem defines :::"push-non-empty"::: STACKS_1:def 12 : (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_stacks_1 :::"push-non-empty"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ))))) ")" )); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ($#v2_stacks_1 :::"pop-finite"::: ) ; cluster (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ($#v3_stacks_1 :::"push-pop"::: ) ; cluster (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ($#v4_stacks_1 :::"top-push"::: ) ; cluster (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ($#v5_stacks_1 :::"pop-push"::: ) ; cluster (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ($#v6_stacks_1 :::"push-non-empty"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_stacks_1 :::"strict"::: ) ($#v2_stacks_1 :::"pop-finite"::: ) ($#v3_stacks_1 :::"push-pop"::: ) ($#v4_stacks_1 :::"top-push"::: ) ($#v5_stacks_1 :::"pop-push"::: ) ($#v6_stacks_1 :::"push-non-empty"::: ) for ($#l1_stacks_1 :::"StackSystem"::: ) ; end; definitionmode StackAlgebra is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_stacks_1 :::"pop-finite"::: ) ($#v3_stacks_1 :::"push-pop"::: ) ($#v4_stacks_1 :::"top-push"::: ) ($#v5_stacks_1 :::"pop-push"::: ) ($#v6_stacks_1 :::"push-non-empty"::: ) ($#l1_stacks_1 :::"StackSystem"::: ) ; end; theorem :: STACKS_1:2 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_stacks_1 :::"pop-finite"::: ) )) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_stacks_1 :::"pop-finite"::: ) ($#l1_stacks_1 :::"StackSystem"::: ) ; cluster (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: STACKS_1:3 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v4_stacks_1 :::"top-push"::: ) ) & (Bool (Set (Var "X")) "is" ($#v5_stacks_1 :::"pop-push"::: ) ) & (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e1")) "," (Set (Var "s1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e2")) "," (Set (Var "s2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Var "e2"))) & (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) ")" )))) ; theorem :: STACKS_1:4 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_stacks_1 :::"StackSystem"::: ) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_stacks_1 :::"push-pop"::: ) ) & (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) & (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s2")))) & (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s2")))) & (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s2"))))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2"))))) ; begin scheme :: STACKS_1:sch 3 INDsch{ F1() -> ($#l1_stacks_1 :::"StackAlgebra":::), F2() -> ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F2 "(" ")" )]) provided (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) "holds" (Bool P1[(Set (Var "s"))])) and (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "s"))])) "holds" (Bool P1[(Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" )]))) proof end; scheme :: STACKS_1:sch 4 EXsch{ F1() -> ($#l1_stacks_1 :::"StackAlgebra":::), F2() -> ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ), F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" )(Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set F1 "(" ")" )) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F2 "(" ")" ))) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) ")" ) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "e")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1")) ")" ) ")" ))) ")" ) ")" ))) proof end; scheme :: STACKS_1:sch 5 UNIQsch{ F1() -> ($#l1_stacks_1 :::"StackAlgebra":::), F2() -> ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ), F3() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) } : (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F3 "(" ")" ) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set F1 "(" ")" )) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F2 "(" ")" ))) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) ")" ) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "e")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1")) ")" ) ")" ))) ")" ) ")" )) & (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set F1 "(" ")" )) "," (Set F3 "(" ")" ) "st" (Bool "(" (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set F2 "(" ")" ))) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) ")" ) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "e")) "," (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1")) ")" ) ")" ))) ")" ) ")" ))) "holds" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "a2")))) proof end; begin definitionlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); let "s" be ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")); func :::"|.":::"s":::".|"::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#k3_finseq_2 :::"*"::: ) ) means :: STACKS_1:def 13 (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X") "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ($#k3_finseq_2 :::"*"::: ) ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) "s")) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1")) ")" )))) ")" ) ")" )); end; :: deftheorem defines :::"|."::: STACKS_1:def 13 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X"))) "," (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#k3_finseq_2 :::"*"::: ) ")" ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "s1")) ")" )))) ")" ) ")" )) ")" )))); theorem :: STACKS_1:5 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: STACKS_1:6 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k6_stacks_1 :::"top"::: ) (Set (Var "s")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_stacks_1 :::"^"::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")) ")" ) ($#k9_stacks_1 :::".|"::: ) ))))) ; theorem :: STACKS_1:7 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")) ")" ) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_stacks_1 :::"Del"::: ) "(" (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) ) "," (Num 1) ")" )))) ; theorem :: STACKS_1:8 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ")" ) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "e")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_stacks_1 :::"^"::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) )))))) ; theorem :: STACKS_1:9 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) ) ($#k1_funct_1 :::"."::: ) (Num 1))))) ; theorem :: STACKS_1:10 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) ; theorem :: STACKS_1:11 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set "(" ($#k8_stacks_1 :::"StandardStackSystem"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))))) ; theorem :: STACKS_1:12 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#k3_finseq_2 :::"*"::: ) ) (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x")))))) ; definitionlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); let "s1", "s2" be ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")); pred "s1" :::"=="::: "s2" means :: STACKS_1:def 14 (Bool (Set ($#k9_stacks_1 :::"|."::: ) "s1" ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) "s2" ($#k9_stacks_1 :::".|"::: ) )); reflexivity (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s1")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s1")) ($#k9_stacks_1 :::".|"::: ) ))) ; symmetry (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")) "st" (Bool (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s1")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s2")) ($#k9_stacks_1 :::".|"::: ) ))) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s2")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s1")) ($#k9_stacks_1 :::".|"::: ) ))) ; end; :: deftheorem defines :::"=="::: STACKS_1:def 14 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2"))) "iff" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s1")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s2")) ($#k9_stacks_1 :::".|"::: ) )) ")" ))); theorem :: STACKS_1:13 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2"))) & (Bool (Set (Var "s2")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s3")))) "holds" (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s3"))))) ; theorem :: STACKS_1:14 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2"))) & (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) "holds" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s2"))))) ; theorem :: STACKS_1:15 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))) & (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s2")))) "holds" (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2"))))) ; theorem :: STACKS_1:16 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2")))) "holds" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ) ($#r2_stacks_1 :::"=="::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s2")) ")" ))))) ; theorem :: STACKS_1:17 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2"))) & (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))))) "holds" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1"))) ($#r2_stacks_1 :::"=="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s2")))))) ; theorem :: STACKS_1:18 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2"))) & (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))))) "holds" (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s2")))))) ; definitionlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); attr "X" is :::"proper-for-identity"::: means :: STACKS_1:def 15 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" "st" (Bool (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2")))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))); end; :: deftheorem defines :::"proper-for-identity"::: STACKS_1:def 15 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v7_stacks_1 :::"proper-for-identity"::: ) ) "iff" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2")))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2")))) ")" )); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ($#v7_stacks_1 :::"proper-for-identity"::: ) ; end; definitionlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); func :::"==_"::: "X" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X") means :: STACKS_1:def 16 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2"))) ")" )); end; :: deftheorem defines :::"==_"::: STACKS_1:def 16 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "s1")) ($#r2_stacks_1 :::"=="::: ) (Set (Var "s2"))) ")" )) ")" ))); registrationlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); cluster (Set ($#k10_stacks_1 :::"==_"::: ) "X") -> ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; theorem :: STACKS_1:19 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" (Set (Var "X")))))) ; definitionlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); let "s" be ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")); func :::"coset"::: "s" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X") means :: STACKS_1:def 17 (Bool "(" (Bool "s" ($#r2_hidden :::"in"::: ) it) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" "st" (Bool (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool "(" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ) ($#r2_hidden :::"in"::: ) it) & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))))) "implies" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1"))) ($#r2_hidden :::"in"::: ) it) ")" ")" )) ")" ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X") "st" (Bool (Bool "s" ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" "st" (Bool (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))))) "implies" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ")" )) ")" )) "holds" (Bool it ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) ")" ); end; :: deftheorem defines :::"coset"::: STACKS_1:def 17 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) "holds" (Bool "(" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))))) "implies" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1"))) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) ")" ")" )) ")" ) & (Bool "(" "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X"))) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))))) "implies" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1"))) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" ")" )) ")" )) "holds" (Bool (Set (Var "b3")) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) ")" ) ")" ) ")" )))); theorem :: STACKS_1:20 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "," (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s1"))))) "implies" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s1")))) ")" & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) & (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s1"))))) "implies" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s1")))) ")" ")" )))) ; theorem :: STACKS_1:21 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ")" ))) & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "implies" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")) ")" ))) ")" ")" )))) ; theorem :: STACKS_1:22 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))) & (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s")))) ")" )))) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "A")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "A" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_FINSET_1() ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_rewrite1 :::"RedSequence"::: ) "of" "R"; end; definitionlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); func :::"ConstructionRed"::: "X" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X") means :: STACKS_1:def 18 (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" "X" "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool "(" (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1")))) ")" ) "or" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" "X" "st" (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"ConstructionRed"::: STACKS_1:def 18 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_stacks_1 :::"ConstructionRed"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "s2")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool "(" (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1")))) ")" ) "or" (Bool "ex" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s1")) ")" ))) ")" ) ")" )) ")" ))); theorem :: STACKS_1:23 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set (Var "R")) "holds" (Bool "(" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) "iff" (Bool (Set (Var "t")) "is" (Set (Var "A")) ($#v5_relat_1 :::"-valued"::: ) ) ")" )))) ; scheme :: STACKS_1:sch 6 PathIND{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Relation":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F3 "(" ")" )]) provided (Bool P1[(Set F2 "(" ")" )]) and (Bool (Set F4 "(" ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set F2 "(" ")" ) "," (Set F3 "(" ")" )) and (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set F4 "(" ")" ) ($#r1_rewrite1 :::"reduces"::: ) (Set F2 "(" ")" ) "," (Set (Var "x"))) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set F4 "(" ")" )) & (Bool P1[(Set (Var "x"))])) "holds" (Bool P1[(Set (Var "y"))])) proof end; theorem :: STACKS_1:24 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "t")) "being" ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k12_stacks_1 :::"ConstructionRed"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Num 1)))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "t"))) ($#r1_tarski :::"c="::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s"))))))) ; theorem :: STACKS_1:25 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "s1")) where s1 "is" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) : (Bool (Set ($#k12_stacks_1 :::"ConstructionRed"::: ) (Set (Var "X"))) ($#r1_rewrite1 :::"reduces"::: ) (Set (Var "s")) "," (Set (Var "s1"))) "}" ))) ; definitionlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); let "s" be ($#m1_subset_1 :::"stack":::) "of" (Set (Const "X")); func :::"core"::: "s" -> ($#m1_subset_1 :::"stack":::) "of" "X" means :: STACKS_1:def 19 (Bool "(" (Bool ($#r1_stacks_1 :::"emp"::: ) it) & (Bool "ex" (Set (Var "t")) "being" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X") ($#v5_relat_1 :::"-valued"::: ) ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k12_stacks_1 :::"ConstructionRed"::: ) "X") "st" (Bool "(" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) "s") & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) it) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "t"))))) "holds" (Bool "(" (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Set (Var "t")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))) & (Bool (Set (Set (Var "t")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set "(" (Set (Var "t")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )) ")" ); end; :: deftheorem defines :::"core"::: STACKS_1:def 19 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k13_stacks_1 :::"core"::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "b3"))) & (Bool "ex" (Set (Var "t")) "being" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_rewrite1 :::"RedSequence"::: ) "of" (Set ($#k12_stacks_1 :::"ConstructionRed"::: ) (Set (Var "X"))) "st" (Bool "(" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "t"))))) "holds" (Bool "(" (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Set (Var "t")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))) & (Bool (Set (Set (Var "t")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set "(" (Set (Var "t")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )) ")" ) ")" ))); theorem :: STACKS_1:26 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k13_stacks_1 :::"core"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))))) ; theorem :: STACKS_1:27 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_stacks_1 :::"core"::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_stacks_1 :::"core"::: ) (Set (Var "s"))))))) ; theorem :: STACKS_1:28 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k13_stacks_1 :::"core"::: ) (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_stacks_1 :::"core"::: ) (Set (Var "s")))))) ; theorem :: STACKS_1:29 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_stacks_1 :::"core"::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s")))))) ; theorem :: STACKS_1:30 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ($#k3_finseq_2 :::"*"::: ) ) (Bool "ex" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s1")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s")))) ")" ))))) ; theorem :: STACKS_1:31 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k13_stacks_1 :::"core"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set ($#k13_stacks_1 :::"core"::: ) (Set (Var "s")))))) ; theorem :: STACKS_1:32 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "s1")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s")))) & (Bool (Set (Var "s2")) ($#r2_hidden :::"in"::: ) (Set ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s")))) & (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s1")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s2")) ($#k9_stacks_1 :::".|"::: ) ))) "holds" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Var "s2"))))) ; theorem :: STACKS_1:33 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Set (Set "(" ($#k11_stacks_1 :::"coset"::: ) (Set (Var "s1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "s")) ($#k6_domain_1 :::"}"::: ) ))))) ; begin definitionlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); func "X" :::"/=="::: -> ($#v1_stacks_1 :::"strict"::: ) ($#l1_stacks_1 :::"StackSystem"::: ) means :: STACKS_1:def 20 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X")) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k10_stacks_1 :::"==_"::: ) "X" ")" ))) & (Bool (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" "X") ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_stacks_1 :::"s_push"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_stacks_1 :::"s_push"::: ) "of" "X") ($#k3_stacks_1 :::"/\/"::: ) (Set "(" ($#k10_stacks_1 :::"==_"::: ) "X" ")" ))) & (Bool (Set "the" ($#u3_stacks_1 :::"s_pop"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u3_stacks_1 :::"s_pop"::: ) "of" "X") ($#k4_stacks_1 :::"+*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" "X") ")" ) ")" ) ($#k2_filter_1 :::"/\/"::: ) (Set "(" ($#k10_stacks_1 :::"==_"::: ) "X" ")" ))) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k10_stacks_1 :::"==_"::: ) "X" ")" )) "holds" (Bool (Set "the" ($#u4_stacks_1 :::"s_top"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u4_stacks_1 :::"s_top"::: ) "of" "X") ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" "X") "," "the" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X") ")" )) ")" ) ")" ); end; :: deftheorem defines :::"/=="::: STACKS_1:def 20 : (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_stacks_1 :::"strict"::: ) ($#l1_stacks_1 :::"StackSystem"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ))) & (Bool (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" (Set (Var "X"))) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_stacks_1 :::"s_push"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_stacks_1 :::"s_push"::: ) "of" (Set (Var "X"))) ($#k3_stacks_1 :::"/\/"::: ) (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ))) & (Bool (Set "the" ($#u3_stacks_1 :::"s_pop"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u3_stacks_1 :::"s_pop"::: ) "of" (Set (Var "X"))) ($#k4_stacks_1 :::"+*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" (Set (Var "X"))) ")" ) ")" ) ($#k2_filter_1 :::"/\/"::: ) (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ))) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_orders_1 :::"Choice_Function"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" )) "holds" (Bool (Set "the" ($#u4_stacks_1 :::"s_top"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u4_stacks_1 :::"s_top"::: ) "of" (Set (Var "X"))) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k2_funct_7 :::"+*"::: ) "(" (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" (Set (Var "X"))) "," "the" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))) ")" )) ")" ) ")" ) ")" ))); registrationlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); cluster (Set "X" ($#k14_stacks_1 :::"/=="::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_stacks_1 :::"strict"::: ) ; end; theorem :: STACKS_1:34 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" ) (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "st" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s")) ")" ))))) ; theorem :: STACKS_1:35 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s")) ")" ) "is" ($#m1_subset_1 :::"stack":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" )))) ; theorem :: STACKS_1:36 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s")) ")" ))) "holds" (Bool "(" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))) "iff" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "S"))) ")" )))) ; theorem :: STACKS_1:37 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" ) "holds" (Bool "(" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "S"))) "iff" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_stacks_1 :::"s_empty"::: ) "of" (Set (Var "X")))) ")" ))) ; theorem :: STACKS_1:38 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Set (Var "E")) ($#r1_hidden :::"="::: ) (Set (Var "e")))) "holds" (Bool "(" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "E")) "," (Set (Var "S")) ")" )) & (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "E")) "," (Set (Var "S")) ")" )) ")" )))))) ; theorem :: STACKS_1:39 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "holds" (Bool "(" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "S")))) & (Bool (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "S")))) ")" )))) ; theorem :: STACKS_1:40 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s")) ")" )) & (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s"))))))) ; registrationlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); cluster (Set "X" ($#k14_stacks_1 :::"/=="::: ) ) -> ($#v1_stacks_1 :::"strict"::: ) ($#v2_stacks_1 :::"pop-finite"::: ) ; cluster (Set "X" ($#k14_stacks_1 :::"/=="::: ) ) -> ($#v1_stacks_1 :::"strict"::: ) ($#v3_stacks_1 :::"push-pop"::: ) ; cluster (Set "X" ($#k14_stacks_1 :::"/=="::: ) ) -> ($#v1_stacks_1 :::"strict"::: ) ($#v4_stacks_1 :::"top-push"::: ) ; cluster (Set "X" ($#k14_stacks_1 :::"/=="::: ) ) -> ($#v1_stacks_1 :::"strict"::: ) ($#v5_stacks_1 :::"pop-push"::: ) ; cluster (Set "X" ($#k14_stacks_1 :::"/=="::: ) ) -> ($#v1_stacks_1 :::"strict"::: ) ($#v6_stacks_1 :::"push-non-empty"::: ) ; end; theorem :: STACKS_1:41 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set "(" (Set (Var "X")) ($#k14_stacks_1 :::"/=="::: ) ")" ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k10_stacks_1 :::"==_"::: ) (Set (Var "X")) ")" ) "," (Set (Var "s")) ")" ))) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "S")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) ))))) ; registrationlet "X" be ($#l1_stacks_1 :::"StackAlgebra":::); cluster (Set "X" ($#k14_stacks_1 :::"/=="::: ) ) -> ($#v1_stacks_1 :::"strict"::: ) ($#v7_stacks_1 :::"proper-for-identity"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_stacks_1 :::"pop-finite"::: ) ($#v3_stacks_1 :::"push-pop"::: ) ($#v4_stacks_1 :::"top-push"::: ) ($#v5_stacks_1 :::"pop-push"::: ) ($#v6_stacks_1 :::"push-non-empty"::: ) ($#v7_stacks_1 :::"proper-for-identity"::: ) for ($#l1_stacks_1 :::"StackSystem"::: ) ; end; begin definitionlet "X1", "X2" be ($#l1_stacks_1 :::"StackAlgebra":::); let "F", "G" be ($#m1_hidden :::"Function":::); pred "F" "," "G" :::"form_isomorphism_between"::: "X1" "," "X2" means :: STACKS_1:def 21 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "F") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X1")) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "F") ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "X2")) & (Bool "F" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "G") ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X1")) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "G") ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "X2")) & (Bool "G" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" "X1" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" "X2" "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set "G" ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "holds" (Bool "(" "(" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) "implies" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s2"))) ")" & "(" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s2")))) "implies" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))) ")" & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))))) "implies" (Bool "(" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set "G" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1")) ")" ))) & (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_stacks_1 :::"top"::: ) (Set (Var "s1")) ")" ))) ")" ) ")" & (Bool "(" "for" (Set (Var "e1")) "being" ($#m1_subset_1 :::"Element":::) "of" "X1" (Bool "for" (Set (Var "e2")) "being" ($#m1_subset_1 :::"Element":::) "of" "X2" "st" (Bool (Bool (Set (Var "e2")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))))) "holds" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e2")) "," (Set (Var "s2")) ")" ) ($#r1_hidden :::"="::: ) (Set "G" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e1")) "," (Set (Var "s1")) ")" ")" )))) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"form_isomorphism_between"::: STACKS_1:def 21 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X1")) "," (Set (Var "X2"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X2")))) & (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X2")))) & (Bool (Set (Var "G")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "holds" (Bool "(" "(" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1")))) "implies" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s2"))) ")" & "(" (Bool (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s2")))) "implies" (Bool ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))) ")" & "(" (Bool (Bool (Bool "not" ($#r1_stacks_1 :::"emp"::: ) (Set (Var "s1"))))) "implies" (Bool "(" (Bool (Set ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_stacks_1 :::"pop"::: ) (Set (Var "s1")) ")" ))) & (Bool (Set ($#k6_stacks_1 :::"top"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_stacks_1 :::"top"::: ) (Set (Var "s1")) ")" ))) ")" ) ")" & (Bool "(" "for" (Set (Var "e1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "e2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "e2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "e1"))))) "holds" (Bool (Set ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e2")) "," (Set (Var "s2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_stacks_1 :::"push"::: ) "(" (Set (Var "e1")) "," (Set (Var "s1")) ")" ")" )))) ")" ) ")" )) ")" ) ")" ) ")" ))); theorem :: STACKS_1:42 (Bool "for" (Set (Var "X")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "X")))) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X")) "," (Set (Var "X")))) ; theorem :: STACKS_1:43 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X1")) "," (Set (Var "X2")))) "holds" (Bool (Set (Set (Var "F")) ($#k2_funct_1 :::"""::: ) ) "," (Set (Set (Var "G")) ($#k2_funct_1 :::"""::: ) ) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X2")) "," (Set (Var "X1"))))) ; theorem :: STACKS_1:44 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "G1")) "," (Set (Var "F2")) "," (Set (Var "G2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "G1")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X1")) "," (Set (Var "X2"))) & (Bool (Set (Var "F2")) "," (Set (Var "G2")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X2")) "," (Set (Var "X3")))) "holds" (Bool (Set (Set (Var "F2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "G1"))) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X1")) "," (Set (Var "X3"))))) ; theorem :: STACKS_1:45 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X1")) "," (Set (Var "X2")))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X2")) "st" (Bool (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "s1"))))) "holds" (Bool (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s2")) ($#k9_stacks_1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s1")) ($#k9_stacks_1 :::".|"::: ) ))))))) ; definitionlet "X1", "X2" be ($#l1_stacks_1 :::"StackAlgebra":::); pred "X1" "," "X2" :::"are_isomorphic"::: means :: STACKS_1:def 22 (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) "X1" "," "X2")); reflexivity (Bool "for" (Set (Var "X1")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X1")) "," (Set (Var "X1"))))) ; symmetry (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) "st" (Bool (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X1")) "," (Set (Var "X2"))))) "holds" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X2")) "," (Set (Var "X1"))))) ; end; :: deftheorem defines :::"are_isomorphic"::: STACKS_1:def 22 : (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) "holds" (Bool "(" (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_stacks_1 :::"are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X1")) "," (Set (Var "X2")))) ")" )); theorem :: STACKS_1:46 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X3")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_stacks_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "X3")) ($#r4_stacks_1 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "X1")) "," (Set (Var "X3")) ($#r4_stacks_1 :::"are_isomorphic"::: ) )) ; theorem :: STACKS_1:47 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#l1_stacks_1 :::"StackAlgebra":::) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "X2")) ($#r4_stacks_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "X1")) "is" ($#v7_stacks_1 :::"proper-for-identity"::: ) )) "holds" (Bool (Set (Var "X2")) "is" ($#v7_stacks_1 :::"proper-for-identity"::: ) )) ; theorem :: STACKS_1:48 (Bool "for" (Set (Var "X")) "being" ($#v7_stacks_1 :::"proper-for-identity"::: ) ($#l1_stacks_1 :::"StackAlgebra":::) (Bool "ex" (Set (Var "G")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool "(" "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"stack":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k9_stacks_1 :::"|."::: ) (Set (Var "s")) ($#k9_stacks_1 :::".|"::: ) )) ")" ) & (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) "," (Set (Var "G")) ($#r3_stacks_1 :::"form_isomorphism_between"::: ) (Set (Var "X")) "," (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X"))))) ")" ))) ; theorem :: STACKS_1:49 (Bool "for" (Set (Var "X")) "being" ($#v7_stacks_1 :::"proper-for-identity"::: ) ($#l1_stacks_1 :::"StackAlgebra":::) "holds" (Bool (Set (Var "X")) "," (Set ($#k8_stacks_1 :::"StandardStackSystem"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ($#r4_stacks_1 :::"are_isomorphic"::: ) )) ;