abkürzung : AG(N,lambda s . P(s)) = AGP


=== good states ===
 
	,->				II0				<-,
	|			<--		-->			  |
	|		WI0				IW0		  |
	|	<--		-->		<--		-->	  |
	CI1				WW0				IC1
		-->		<--		-->		<--
			CW1				WC1
		
		CW1 -> IW0 	
		WC1 -> WI0
		
		
=== bad states ===		
		
		II1
	<--		-->
WI1				IW1
	-->		<--
		WW1
		
				II0 (good)
			-->		<--
		IC0				CI0
	<--		<--		-->		-->
WC0				CC0				CW0
	
		CCI -> CI1 (bad->good)
		CCI -> iC1 (bad->good)
		
=== NR 28 ===

|=/= ist ein durchgestrichenes |=

A1 = AG (pc1 = w & pc2 = c)

	WW0 |=/= pc1 = w => pc2 = c
	WW0 |=/= AG(pc1 = w => pc2 = c)

A2 = pc1 = w & pc2 = I => AX ( pc1 = C )    [optional dazu :   & EX (pc1 = c) ]

	WIO |=/= A2
	
A3 : alt1  II0 |= ( AF ( A2 )) & ( EF ( A2 ))
	wahr, da II0 |= A2

A4 : II0 |=   AG ( EX ( true ) /\ AF ( OC ) ) 
	wobei : OC = pc1 = C \/ pc2 = c 
	EX ( true ) heisst : das system bleibt nicht stecken
	
A5 : II0 |= AG ( AF ( pc1 = C) /\  EX (t) )
	falsch, da auf dem undendlichen pfad  ( WIO , WW0 , WC0 , WIO ...)   pc1 != c  und WI0 ist von II0 erreichbar

=== Nr.29.1 ===

in : teilmenge oder gleich
el : element

fi ^ i : fi "hoch" i , also i als index rechtsoben (i-fache anwendung der funktion)

|_| : vereinigungsmenge

|^| : schnittmenge

fi : M -> M   A in B  -> fi(A) in fi(B)

A =   |_|  fi ^ i (0)     B =   |^|    Q
	i el N					 fi(Q) in Q

1. zeige fi(B) in B =       |^|      Q
						fi(Q) in Q

	Für bel Q.--    fi(Q) in Q   zeige fi(B) in Q
	
						monotonie
	Es gilt: B in Q    ==========> fi (B) in fi(Q) in Q   q.e.d

	Zeige A =   |_|   fi^i (0)   in B
			  i el N
			  
	genügt zz.: fi^i(0) in B  Für alle i in N     (dann ist Vereinigung auch in B)
	
	Induktion über i : 
		i=0 : 		fi ^ 0 (0)  =  0   in  B
		
		i+i:		IV.   fi^i (0)  in B
			
					fi ^ (i+1) (0) = fi( fi^i ( 0 ))       
					
			(IV,Monotonie :)     rechte seite    in fi(B)   in  	 B    q.e.d.
															(s.o.)
	
=== Nr.29.2 ===
	
	lm  :  leere menge
	zeichen : fi ohne parameter : leere menge
	
	M endlich     lm  in  fi (0) 
				----------------  	mon     lm  IN  fi(0)  IN  fi(fi(0))  IN
				fi(0) in fi(fi(0))
	
	zeige zuerst :  fi^n ( lm )  IN   fi ^ (n+1) ( lm)   durch induktion nach n
	zeige dann      | fi ^ (n+1) |  >= n+1    \/   fi^(n+1)  =  fi^n (0)   durch induktion nach n
		n=0		zz:    |fi(0)| >= 1   \/  fi(0)  = 0
		n+1		nach I.V.  gilt entweder
				a)  fi^(n+1)(0) >= n+1     Da fi ^ (n+2) (0)  IN   fi^(n+1)(0)
											ist | fi ^ (n+1)(0) | >= n+1  also
											entweder | fi^(n+1)(0) |   oder  | fi^(n+2)(0) | = n+1 
											dann aber   fi^(n+2) (0) = fi^(n+1) (0)
				b) fi^(n+1)(0) = fi^n(0)
					Dann fi^(n+2)(0)  =  fi^(n+1)(0), da fi funktion
					
		Da M endlich ist,  und  fi^i(0)  IN  M
		ist  fi^(|M|+1)(0)  >=  |M| + 1   widersprüchlich
		also gilt fi^(|M|+1)(0) = fi^(|M|) (0)
		
		Also  n0 = |M|  und  fi ^ (n0+i) (lm)  =  fi^(n0) (0)      (durch ind. nach i)

=== Nr.29.2.2 ===

	zz :  fi(A) IN A
	
	A =   |_|  fi^i ( 0 )  =  fi^(n0)(0)
		i el N
	
	fi(fi^(n0)(0)) = fi^(n0+1)(0) = fi^n0 ( 0 )
	
	zz : B in A
	
	   |^|   Q    IN   A , da  A  in  { Q | fi (Q) IN Q  }
	fi(Q) in Q
	


=== NR.30 ===
	
	nichtdeterministische nachrichtenfindung : 	2 möglichkeiten :
	
	a)  Exists b mit    msg := b    (probleme mit unendlichem typraum)
	b)  2 übergänge , einer nach   msg=true, einer nach msg=false