$\infer[/ L]{
		(np\ /\ n)\circ n\circ((n\ \bs\ n)\ /\ (s/\Diamond\Box np))\circ np\circ (np\ \bs\ s)\circ \langle((\Box((np\ \bs\ s)\ \bs\ (np\bs\ s)))\ /\ np)\rangle \Rightarrow np
	} {
		\infer[Ax] {
			np \Rightarrow np
		} {}
		&
		\infer[/L] {
			n\circ((n\ \bs\ n)\ /\ (s/\Diamond\Box np))\circ np\circ (np\ \bs\ s)\circ \langle((\Box((np\ \bs\ s)\ \bs\ (np\bs\ s)))\ /\ np)\rangle \Rightarrow n
		} {
			\infer[\bs L] {
				n \circ (n\bs n) \Rightarrow n
			} {
				\infer[Ax] {
					n \Ra n
				} {}
				&
				\infer[Ax] {
					n\Ra n
				} {}
			}
			&
			\infer[/R] {
			np\circ (np\ \bs\ s)\circ \langle((\Box((np\ \bs\ s)\ \bs\ (np\bs\ s)))\ /\ np)\rangle \Ra s/\Diamond\Box np
			} {
			 	\infer[\Diamond L] {
			 		 (np\circ (np\ \bs\ s)\circ \langle((\Box((np\ \bs\ s)\ \bs\ (np\bs\ s)))\ /\ np)\rangle)\circ \Diamond\Box np \Ra s
			 	} {
				 	 \infer[P1] {
				 	 	(np\circ (np\ \bs\ s)\circ (\langle((\Box((np\ \bs\ s)\ \bs\ (np\bs\ s)))\ /\ np)\rangle)\circ\langle\Box np\rangle \Ra s
			 	 	} {
			 	 		\infer[P1] {
			 	 				np\circ ((np\ \bs\ s)\circ (\langle((\Box((np\ \bs\ s)\ \bs\ (np\bs\ s)))\ /\ np)\rangle)\circ\langle\Box np\rangle)  \Ra s
			 	 		}{
			 	 				\infer[\Box L] {
					 	 		np\circ (np\ \bs\ s)\circ \langle((\Box((np\ \bs\ s)\ \bs\ (np\bs\ s)))\ /\ np)\rangle\circ\langle\Box np\rangle  \Ra s
					 	 	} {
					 	 		\infer[\textrm{\lightning}] {
					 	 			np\circ (np\ \bs\ s)\circ \langle((\Box((np\ \bs\ s)\ \bs\ (np\bs\ s)))\ /\ np)\circ np\rangle  \Ra s
					 	 		} {
					 	 			\textrm{\Lightning}
					 	 		}
					 	 	}
			 	 		}
			 	 	}
			 	}
			}
		}
	}
$