:: SCHEMS_1  semantic presentation begin  




scheme  :: SCHEMS_1:sch 1 Schemat0{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a"))]))
 provided
(Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a"))]))
 proof 


end; scheme  :: SCHEMS_1:sch 2 Schemat3{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))])))
 provided
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "b"))])))
 proof 


end; scheme  :: SCHEMS_1:sch 3 Schemat8{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
 "("  (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a"))])  ")" )) "implies" (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P2[(Set (Var "a"))]))  ")" 
 provided
(Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "a"))])) "holds"  (Bool P2[(Set (Var "a"))]))
 proof 


end; scheme  :: SCHEMS_1:sch 4 Schemat9{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "("  (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a"))])  ")" ) "iff" (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P2[(Set (Var "a"))]))  ")" )
 provided
(Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool P1[(Set (Var "a"))]) "iff" (Bool P2[(Set (Var "a"))])  ")" ))
 proof 


end; scheme  :: SCHEMS_1:sch 5 Schemat17{ P1[   ($#m1_hidden :::"set"::: )  ], P2[] } : 
 "("  (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a"))])  ")" )) "implies" (Bool P2[])  ")" 
 provided
(Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "a"))])) "holds"  (Bool P2[]))
 proof 


end; scheme  :: SCHEMS_1:sch 6 Schemat18a{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool P1[(Set (Var "a"))]) "or" (Bool P2[(Set (Var "b"))])  ")" )))
 provided
(Bool  "("  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a"))])) "or" (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P2[(Set (Var "b"))]))  ")" )
 proof 


end; scheme  :: SCHEMS_1:sch 7 Schemat18b{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "("  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a"))])) "or" (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P2[(Set (Var "b"))]))  ")" )
 provided
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool P1[(Set (Var "a"))]) "or" (Bool P2[(Set (Var "b"))])  ")" )))
 proof 


end; scheme  :: SCHEMS_1:sch 8 Schemat20b{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool P1[(Set (Var "a"))]) "or" (Bool P2[(Set (Var "b"))])  ")" )))
 provided
(Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool P1[(Set (Var "a"))]) "or" (Bool P2[(Set (Var "b"))])  ")" )))
 proof 


end; scheme  :: SCHEMS_1:sch 9 Schemat22a{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "b"))])  ")" )))
 provided
(Bool  "("  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a"))])) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P2[(Set (Var "b"))])  ")" )  ")" )
 proof 


end; scheme  :: SCHEMS_1:sch 10 Schemat22b{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "("  (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a"))])) & (Bool  "("   "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P2[(Set (Var "b"))])  ")" )  ")" )
 provided
(Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "b"))])  ")" )))
 proof 


end; scheme  :: SCHEMS_1:sch 11 Schemat23b{ P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "b"))])  ")" )))
 provided
(Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool P1[(Set (Var "a"))]) & (Bool P2[(Set (Var "b"))])  ")" )))
 proof 


end; scheme  :: SCHEMS_1:sch 12 Schemat28{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "b"))])))
 provided
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "b"))]))
 proof 


end; scheme  :: SCHEMS_1:sch 13 Schemat30{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a")) "," (Set (Var "a"))]))
 provided
(Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "b"))])))
 proof 


end; scheme  :: SCHEMS_1:sch 14 Schemat31{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "b")) "," (Set (Var "a"))])))
 provided
(Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "a"))]))
 proof 


end; scheme  :: SCHEMS_1:sch 15 Schemat33{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))])))
 provided
(Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool P1[(Set (Var "a")) "," (Set (Var "a"))]))
 proof 


end; scheme  :: SCHEMS_1:sch 16 Schemat36{ P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))]))
 provided
(Bool  "for" (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))])))
 proof 


end;